Operation Calls in Expressions

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

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