Design by Contract for statecharts

About Design by Contract

Design by Contract (DbC) was introduced by Bertrand Meyer and popularised through his object-oriented Eiffel programming language. Several other programming languages also provide support for DbC. The main idea is that the specification of a software component (e.g., a method, function or class) is extended with a so-called contract that needs to be respected when using this component. Typically, the contract is expressed in terms of preconditions, postconditions and invariants. We have additionally added so-called sequential conditions on top of this.

Design by contract (DbC), also known as contract programming, programming by contract and design-by-contract programming, is an approach for designing software. It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants. These specifications are referred to as “contracts”, in accordance with a conceptual metaphor with the conditions and obligations of business contracts. — Wikipedia

DbC for statechart models

While DbC has gained some amount of acceptance at the programming level, there is hardly any support for it at the modeling level.

Sismic aims to change this, by integrating support for Design by Contract for statecharts. The basic idea is that contracts can be defined on statechart componnents (states or transitions), by specifying preconditions, postconditions, invariants and sequential conditions (i.e. conditions that must be sequentially satisfied) on them. At runtime, Sismic will verify the conditions specified by the constracts. If a condition is not satisfied, a ContractError will be raised. More specifically, one of the following 4 error types wil be raised: PreconditionError, PostconditionError, InvariantError, or SequentialConditionError.

Contracts can be specified for any state contained in the statechart, and for any transition contained in the statechart. A state contract can contain preconditions, postconditions, invariants and/or sequential conditions. At transition level, sequential conditions are not allowed. The semantics for evaluating a contract is as follows:

  • For states:
    • state preconditions are checked before the state is entered (i.e., before executing on entry), in the order of occurrence of the preconditions.
    • state postconditions are checked after the state is exited (i.e., after executing on exit), in the order of occurrence of the postconditions.
    • state invariants are checked at the end of each macro step, in the order of occurrence of the invariants. The state must be in the active configuration.
    • sequential conditions on a state are initialized after a state is entered (i.e., after executing on entry), and evaluated before the state is exited (i.e., before executing on exit). The evaluation of the sequential condition is updated at each step as long as the state remains in the active configuration.
  • For transitions:
    • the preconditions are checked before starting the process of the transition (and before executing the optional transition action).
    • the postconditions are checked after finishing the process of the transition (and after executing the optional transition action).
    • the invariants are checked twice: one before starting and a second time after finishing the process of the transition.

Defining contracts in YAML

Contracts can easily be added to the YAML definition of a statechart (see Defining statecharts in YAML) through the use of the contract property. Preconditions, postconditions, invariants and sequential conditions are defined as nested items of the contract property. The name of these optional contractual conditions is respectively before (for preconditions), after (for postconditions), always (for invariants), and sequentially (for sequential conditions):

contract:
 - before: ...
 - after: ...
 - always: ...
 - sequentially: ...

Obviously, more than one condition of each type can be specified:

contract:
 - before: ...
 - before: ...
 - before: ...
 - after: ...

A condition is an expression that will be evaluated by an Evaluator instance (see Include code in statecharts).

contract:
 - before: x > 0
 - before: y > 0
 - after: x + y == 0
 - always: x + y >= 0

Here is an example of a contracts defined at state level:

statechart:
  name: example
  root state:
    name: root
    contract:
     - always: x >= 0
     - always: not active('other state') or x > 0

If the default PythonEvaluator is used, it is possible to refer to the old value of some variable used in the statechart, by prepending __old__. This is particularly useful when specifying postconditions and invariants:

contract:
  always: d > __old__.d
  after: (x - __old__.x) < d

See the documentation of PythonEvaluator for more information.

Sequential conditions

Sequential conditions can be used to describe what should happen when residing in a particular state, and in which order. A sequential condition makes use of some logical and temporal operators, and of classical conditions that will be evaluated by an Evaluator instance (by default, a PythonEvaluator one).

Refer to the documentation of build_sequence() for more information about the supported operators. You will never call this function directly, but the documentation explains the implemented mini-language and the supported operators and their semantics.

sismic.code.sequence.build_sequence(expression: str, evaluation_function: typing.Callable[[str], bool] = <built-in function eval>) → sismic.code.sequence.Sequence

Parse an expression and return the corresponding sequence according to the following mini-language:

  • atom:
    • “code” or ‘code’: a fragment of code (e.g. Python code) representing a Boolean expression that evaluates to true or false. The semantics is “satisfied once”: as soon as the code evaluates to true once, the truth value of the expression remains true. This is equivalent as “sometimes ‘code’” in linear temporal logic.
  • constants:
    • failure: this constant always evaluates to false.
    • success: this constant always evaluates to true.
  • unary operators:
    • never A: this expression evaluates to false as soon as expression A evaluates to true.
  • binary operators:
    • A and B: logical and
    • A or B: logical or
    • A -> B: this is equivalent to “(next always B) since A” in linear temporal logic, i.e. B has to be true (strictly) since A holds. Notice that, due to the “satisfied once” semantics of the atoms, if A and B are atoms, this is merely equivalent to “(A and next (sometimes B))”, which means A needs to be true strictly before B or, in other words, A must be satisfied once, then B must be holds once.

Keywords are case-insensitive. Parentheses can be used to group sub expressions. Unary operators have precedence over binary ones (e.g. “A and never B” is equivalent to “A and (never B)”). Unary operators are right associative while binary operators are left associative (e.g. “A and B and C” is equivalent to “(A and B) and C”). The binary operators are listed in decreasing priority (e.g. “A or B and C” is equivalent to “A or (B and C)”, and “A and B -> C or D” is equivalent to “(A and B) -> (C or D)”).

Examples (assuming that expressions between quotes can be evaluated to true or false):

  • “put water” -> “put coffee”: ensures water is put before coffee.
  • “put water” and “put coffee”: ensures water and coffee are put. Due to the “satisfied once” semantics of the atoms, the order in which items are put does not matter.
  • (never “put water”) or (“put water” -> “put coffee”): if water is put, then coffee must be put too.
  • never (“put water” -> “put water”): the condition will fail if water is put twice (but will succeed if water is put once or never put).
  • “put water” -> (never “put water”): put water exactly once.
Parameters:
  • expression – an expression to parse
  • evaluation_function – the function that will be called to evaluate nested pieces of code
Returns:

a Sequence instance.

Please be warned: the syntax allowed in sequential conditions may conflict with YAML’s one. Protect your sequential conditions by using quotes or by using the multi-line marker “|”.

Example

The following example shows some contract specifications added to the Elevator example.

statechart:
  name: Elevator
  preamble: |
    current = 0
    destination = 0
    doors_open = True
  root state:
    name: active
    contract:
      - before: current == 0
      - always: current >= 0  # Floor must be valid
      - always: destination >= 0  # Selected floor must be valid
    parallel states:
      - name: movingElevator
        initial: doorsOpen
        states:
          - name: doorsOpen
            transitions:
              - target: doorsClosed
                guard: destination != current
                action: doors_open = False
              - target: doorsClosed
                guard: after(10) and current > 0
                action: |
                  destination = 0
                  doors_open = False
                contract:
                  - before: current > 0
                  - after: destination == 0
          - name: doorsClosed
            transitions:
              - target: movingUp
                guard: destination > current
              - target: movingDown
                guard: destination < current and destination >= 0
          - name: moving
            contract:
              - always: not doors_open  # Keep doors closed while moving
              - before: destination != current  # Move only if destination is not reached
              - after: destination == current  # Destination should be reached
              - after: current != __old__.current  # Current changed (redundant given the two last conditions)
              - sequentially: |
                  (
                    ("destination > current" -> "current > __old__.current")
                    or ("destination < current" -> "current < __old__.current")
                  ) -> "destination == current"
            transitions:
              - target: doorsOpen
                guard: destination == current
                action: doors_open = True
                contract:
                  - before: not doors_open  # Doors are closed
                  - after: doors_open  # Doors are opened
            states:
              - name: movingUp
                on entry: current = current + 1
                contract:
                  - before: current < destination  # Move up only if below
                  - always: current <= destination  # Never go above destination
                  - after: current > __old__.current  # Move up!
                transitions:
                  - target: movingUp
                    guard: destination > current
              - name: movingDown
                contract:
                  - before: current > destination  # Move down only if above
                  - always: current >= destination  # Never go below destination
                  - after: current < __old__.current  # Move down!
                on entry: current = current - 1
                transitions:
                  - target: movingDown
                    guard: destination < current
      - name: floorListener
        initial: floorSelecting
        contract:
          - sequentially: "'received(\"floorSelected\")' -> 'current == destination' or ('current != destination' -> 'current == destination')"
        states:
          - name: floorSelecting
            transitions:
              - target: floorSelecting
                event: floorSelected
                action: destination = event.floor

Executing statecharts containing contracts

The execution of a statechart that contains contracts does not essentially differ from the execution of a statechart that does not. The only difference is that conditions of each contract are checked at runtime (as explained above) and may raise a subclass of ContractError.

from sismic.model import Event
from sismic.interpreter import Interpreter
from sismic.io import import_from_yaml

with open('examples/elevator/elevator_contract.yaml') as f:
    statechart = import_from_yaml(f)

    # Make the run fails
    statechart.state_for('movingUp').preconditions[0] = 'current > destination'

    interpreter = Interpreter(statechart)
    interpreter.queue(Event('floorSelected', floor=4))
    interpreter.execute()

Here we manually changed one of the preconditions such that it failed at runtime. The exception displays some relevant information to help debug:

Traceback (most recent call last):
 ...
sismic.exceptions.PreconditionError: PreconditionError
Object: BasicState('movingUp')
Assertion: current > destination
Configuration: ['active', 'floorListener', 'movingElevator', 'floorSelecting', 'moving']
Step: MicroStep(transition=Transition('doorsClosed', 'movingUp', event=None), entered_states=['moving', 'movingUp'], exited_states=['doorsClosed'])
Context:
 - current = 0
 - destination = 4
 - doors_open = False

If you do not want the execution to be interrupted by such exceptions, you can set the ignore_contract parameter to True when constructing an Interpreter. This way, no contract checking will be done during the execution.