No edit summary |
|||
(5 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
[[Category:User Manual]] | [[Category:User Manual]] | ||
[[Category: Advanced Feature]] | [[Category: Advanced Feature]] | ||
= Symbolic Functions and Relations = | |||
Take the following function: | Take the following function: | ||
CONSTANTS parity | CONSTANTS parity | ||
Line 67: | Line 68: | ||
* <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left. | * <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left. | ||
* the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>) | * the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>) | ||
* a pragma is used to mark the lambda abstraction as symbolic as follows <tt>f = /*@ symbolic */ %x.(PRED|E)</tt>; this requires ProB version 1.3.5-beta10 or higher. | * a pragma is used to mark the lambda abstraction as symbolic as follows: <tt>f = /*@ symbolic */ %x.(PRED|E)</tt>; this requires ProB version 1.3.5-beta10 or higher. In Event-B, pragmas are represented as Rodin database attributes and one should use the [[Tutorial_Symbolic_Constants|symbolic constants plugin]]. | ||
= Recursive Function Definitions in ProB = | = Recursive Function Definitions in ProB = | ||
Line 83: | Line 83: | ||
parity : INTEGER <-> INTEGER & | parity : INTEGER <-> INTEGER & | ||
parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1)) | parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1)) | ||
END | |||
As of version 1.6.1 you can also use IF-THEN-ELSE and LET constructs in the body of a recursive function. The above example can for example now be written as: | |||
MACHINE ParityIFTE | |||
ABSTRACT_CONSTANTS parity | |||
PROPERTIES | |||
parity : INTEGER <-> INTEGER & | |||
parity = %x.(x:NATURAL|IF x=0 THEN 0 ELSE 1-parity(x-1)END) | |||
END | END | ||
Line 89: | Line 97: | ||
* apply the function to a given argument, e.g., <tt>parity(100)</tt> will give you 0; | * apply the function to a given argument, e.g., <tt>parity(100)</tt> will give you 0; | ||
* compute the image of the function, e.g., <tt>parity[1..10]</tt> gives <tt>{0,1}</tt>. | * compute the image of the function, e.g., <tt>parity[1..10]</tt> gives <tt>{0,1}</tt>. | ||
* composing it with another function, notably finite sequences: <tt>([1,2] ; parity)</tt> corresponds to the "map" construct of functional programming and results in the output <tt>[1,0]</tt>. | |||
Also, you have to be careful to avoid accidentally expanding these functions. For example, trying to check <tt>parity : INTEGER <-> INTEGER</tt> or <tt>parity : INTEGER +-> INTEGER</tt> will cause ProB to try and expand the function. | Also, you have to be careful to avoid accidentally expanding these functions. For example, trying to check <tt>parity : INTEGER <-> INTEGER</tt> or <tt>parity : INTEGER +-> INTEGER</tt> will cause older version of ProB to try and expand the function. ProB 1.6.1 can actually check <tt>parity:NATURAL --> INTEGER</tt>, but it cannot check <tt>parity:NATURAL --> 0..1</tt>. | ||
There are the following further restrictions: | There are the following further restrictions: | ||
* ProB does not support mutual recursion yet | * ProB does not support mutual recursion yet | ||
* the function is not allowed to depend on other constants, unless those other constants can be valued in a deterministic way (i.e., ProB finds only one possible solution for them) | * the function is not allowed to depend on other constants, unless those other constants can be valued in a deterministic way (i.e., ProB finds only one possible solution for them) |
Take the following function:
CONSTANTS parity PROPERTIES parity : (NATURAL --> {0,1}) & parity(0) = 0 & !x.(x:NATURAL => parity(x+1) = 1 - parity(x))
Here, ProB will complain that it cannot find a solution for parity. The reason is that parity is a function over an infinite domain, but ProB tries to represent the function as a finite set of maplets.
There are basically four solutions to this problem:
parity : (NAT --> {0,1}) & parity(0) = 0 & !x.(x:NAT & x<MAXINT => parity(x+1) = 1 - parity(x))
parity : (NATURAL --> {0,1}) & parity(0) = 0 & !x.(x:NATURAL1 => parity(x) = 1 - parity(x-1))
parity : INTEGER <-> INTEGER & parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1))
Note, you have to remove the check parity : (NATURAL --> {0,1}), as this will currently cause expansion of the recursive function. We describe this new scheme in more detail below.
parity : (NATURAL --> INTEGER) & parity = %x.(x:NATURAL|x mod 2)
You can experiment with those by using the Eval console of ProB, experimenting for example with the following complete machine. Note, you should use ProB 1.3.5-beta2 or higher.
(You can also type expressions and predicates such as parity = %x.(x:NATURAL|x mod 2) & parity[1..10] = res directly into the online version of the Eval console).
MACHINE InfiniteParityFunction CONSTANTS parity PROPERTIES parity : NATURAL --> INTEGER & parity = %x.(x:NATURAL|x mod 2) VARIABLES c INVARIANT c: NATURAL INITIALISATION c:=0 OPERATIONS Inc = BEGIN c:=c+1 END; r <-- Parity = BEGIN r:= parity(c) END; r <-- ParityImage = BEGIN r:= parity[0..c] END; r <-- ParityHistory = BEGIN r:= (%i.(i:1..c+1|i-1) ; parity) END END
You may also want to look at the tutorial page on modeling infinite datatypes.
Currently there are four cases when ProB tries to keep a function such as f = %x.(PRED|E) symbolically rather than computing an explicit representation:
As of version 1.3.5-beta7 ProB now accepts recursively defined functions. For this:
Here is a full example:
MACHINE Parity ABSTRACT_CONSTANTS parity PROPERTIES parity : INTEGER <-> INTEGER & parity = {0|->0} \/ %x.(x:NATURAL1|1-parity(x-1)) END
As of version 1.6.1 you can also use IF-THEN-ELSE and LET constructs in the body of a recursive function. The above example can for example now be written as:
MACHINE ParityIFTE ABSTRACT_CONSTANTS parity PROPERTIES parity : INTEGER <-> INTEGER & parity = %x.(x:NATURAL|IF x=0 THEN 0 ELSE 1-parity(x-1)END) END
With such a recursive function you can:
Also, you have to be careful to avoid accidentally expanding these functions. For example, trying to check parity : INTEGER <-> INTEGER or parity : INTEGER +-> INTEGER will cause older version of ProB to try and expand the function. ProB 1.6.1 can actually check parity:NATURAL --> INTEGER, but it cannot check parity:NATURAL --> 0..1.
There are the following further restrictions: