Operation Calls in Expressions - Revision history

Michael Leuschel at 13:51, 16 April 2020

2020-04-16T13:51:12Z

← Older revision		Revision as of 13:51, 16 April 2020
Line 64:		Line 64:
	* The PROPERTIES clause.		* The PROPERTIES clause.
	Reason: the operations can depend on variables; the PROPERTIES talks only about constants.		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.)		In future, we could allow using operation calls to fully static operations, not using variables and constants or just static operations of subsidiary machines.
	* The INITIALISATION clause.		* The INITIALISATION clause.
	Reason: the operations can depend on variables; the INITIALISATION cannot read variables.		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.		We could allow using operation calls to “static” operations in the INITIALISATION and possibly operations of already initialised subsidiary machines.

Michael Leuschel at 10:43, 16 April 2020

2020-04-16T10:43:14Z

@@ Line 12: / Line 12: @@
 * sometimes, it is more efficient to express a function this way
 * one can add preconditions (using PRE) to the functions
 Take the following example.
@@ Line 47: / Line 49: @@
 END
 </pre>

Michael Leuschel at 10:39, 16 April 2020

2020-04-16T10:39:00Z

← Older revision		Revision as of 10:39, 16 April 2020
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.

	~~Take the following example:~~
	<pre>		<pre>
	MACHINE CallQueryOperationInExpression		MACHINE CallQueryOperationInExpression

Michael Leuschel: 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..."

2020-04-16T10:34:51Z

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..."

New page

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 <tt>ALLOW_OPERATION_CALLS_IN_EXPRESSIONS</tt> to TRUE.

Take the following example:
<pre>
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
</pre>