Operation Calls in Expressions: Difference between revisions

As of version 1.10.0 ProB allows you to call query operations in expressions. In general, B forbids to call operations in expressions: an operation is a substitution which can change the state, an expression is evaluated in a given state and does not modify it. Also, the correctness of operations typically relies on the INVARIANT to hold, while expressions can be evaluated in many contexts, e.g., in the middle of an operation where the invariant is not yet re-established.

In this new experimental feature, ProB allows to call query operations (which do not modify the state) within certain expressions (where it is guaranteed that the invariant holds or is not required). To enable the feature one needs to set the preference ALLOW_OPERATION_CALLS_IN_EXPRESSIONS to TRUE.

The motivation is as follows:

• sometimes it is more convenient to express a function as a substitution, e.g., using WHILE loops
• sometimes, it is more efficient to express a function this way
• one can add preconditions (using PRE) to the functions
• one can add ASSERT statements within the operation
• Operations can access the current state of variables: the return value can depend on the current state of the B machine

Take the following example. One can see that the two query operations Double and Divisors can be called in the ASSERTIONS clause.

 MACHINE CallQueryOperationInExpression
DEFINITIONS SET_PREF_ALLOW_OPERATION_CALLS_IN_EXPRESSIONS == TRUE
SETS
 ID={aa,bb}
VARIABLES jj
INVARIANT
 jj:ID
INITIALISATION jj:=aa
OPERATIONS
  r <-- Double(x) = PRE x:0..255 THEN r := (x+x) mod 255 END;
  r <-- Divisors(x) = PRE x:1..255 THEN
         VAR i,j IN
            i := 1; j:=0;
            WHILE i <= x DO
              IF x mod i = 0 THEN j := j+1 END;
              i:=i+1
              INVARIANT i : 1..(x+1)
              VARIANT x-i
            END;
            r := j
         END
        END;
  r <-- Test = BEGIN r := Divisors(Double(2)*Double(3)) END
ASSERTIONS
  Double(2) = 4;
  Double(128) = 1;
  Divisors(3) = 2;
  Divisors(4) = 3
END

Operation calls to expressions are currently allowed in

• In the ASSERTIONS clause
• In the bodies of operations with the following restrictions:
  • Operations of the same machine can only be called in query operations, because otherwise the invariant may not hold (in the middle of the calling operation). [Note: this is currently not checked in ProB yet.] We could allow to call query operations that do not depend on variables everywhere.
  • Operations of subsidiary (included,...) machines can be called everywhere
• In the REPL (B console) of ProB

Operation calls in expressions are currently not allowed in:

• the INVARIANT clause, unless one calls operations in included/seen/used machines.

Reason: the correctness of the operation can depend on the invariant being true. If the INVARIANT itself calls the operation we have a potential circular reasoning and problem.

• The PROPERTIES clause.

Reason: the operations can depend on variables; the PROPERTIES talks only about constants. We could allow using operation calls to “static” operations in the PROPERTIES.QUESTION: do we allow these operations to use constants? When called during checking the PROPERTIES we are not sure they hold; there could be a cycle while conducting proof. (I prefer to allow only fully static operations, not using variables and constants or just static operations of subsidiary machines.)

• The INITIALISATION clause.

Reason: the operations can depend on variables; the INITIALISATION cannot read variables. We could allow using operation calls to “static” operations in the INITIALISATION and possibly operations of already initialised subsidiary machines.