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.

Take the following example:

 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