(Created page with " 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 c...") |
No edit summary |
||

Line 8: | Line 8: | ||

To enable the feature one needs to set the preference <tt>ALLOW_OPERATION_CALLS_IN_EXPRESSIONS</tt> to TRUE. | To enable the feature one needs to set the preference <tt>ALLOW_OPERATION_CALLS_IN_EXPRESSIONS</tt> 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. | |||

<pre> | <pre> | ||

MACHINE CallQueryOperationInExpression | MACHINE CallQueryOperationInExpression |

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