m (→Preferences: changed "often" to frequently, changed word order) |
m (grammatical edits, punctuation edits) |
||
Line 15: | Line 15: | ||
specification: There must be a schema called "Init". | specification: There must be a schema called "Init". | ||
"Init" describes the initialisation of the state. | "Init" describes the initialisation of the state. | ||
"Init" must include exactly one schema in the declaration part | "Init" must include exactly one schema in the declaration part. This schema is assumed to be the state schema. | ||
For example, let S be the state schema (= is used for \defs): | For example, let S be the state schema (= is used for \defs): | ||
Line 26: | Line 25: | ||
b) Init = [ S'| x'=0 /\ y'=1 ] | b) Init = [ S'| x'=0 /\ y'=1 ] | ||
If you want to use the logic of other schemas | If you want to use the logic of other schemas besides the state schema | ||
in the initialisation, you can do that by including those schemas in the predicate part. | in the initialisation, you can do that by including those schemas in the predicate part. | ||
Line 44: | Line 43: | ||
F = [ \Xi S | x=0 ] | F = [ \Xi S | x=0 ] | ||
Then the schemas A,B and E describe all the same operation | Then the schemas A,B and E describe all the same operation. F is also identified as an operation that leaves the state unchanged. | ||
=== Axiomatic definitions === | === Axiomatic definitions === | ||
If axiomatic definitions are present, the declared variables are treated like constants. In the first step of the animation, ProB searches for values that satisfy all predicates of the axiomatic definitions are searched. | If axiomatic definitions are present, the declared variables are treated like constants. In the first step of the animation, ProB searches for values that satisfy all predicates of the axiomatic definitions are searched. | ||
After the first step the predicates of the axiomatic definitions | After the first step, the predicates of the axiomatic definitions | ||
are ignored. | are ignored. | ||
If you want to define functions in an axiomatic definition, consider that ProB can treat lambda expressions and set comprehensions symbolically. | If you want to define functions in an axiomatic definition, consider that ProB can treat lambda expressions and set comprehensions symbolically. | ||
Line 64: | Line 63: | ||
| \forall x:Z @ square x = x*x | | \forall x:Z @ square x = x*x | ||
When using ProZ, it is preferable to use the method "a" because the lambda expression can be interpreted symbolically. If "b" is used, ProB will try to find a explicit set that will satisfy the given property. | |||
=== Invariant === | === Invariant === | ||
Line 79: | Line 78: | ||
Abbreviation definitions (e.g. Abbr == {1,2,3}) are used like macros by | Abbreviation definitions (e.g. Abbr == {1,2,3}) are used like macros by | ||
ProZ | ProZ. A reference to an abbreviation is replaced by its definition in | ||
a preprocessor phase. | a preprocessor phase. | ||
Thereby schemas defined by abbreviation definitions are ignored when | Thereby schemas defined by abbreviation definitions are ignored when | ||
ProZ tries to identify components. So use schema definitions instead of abbreviation definitions (\defs instead of ==) when defining state, initialisation, operations, etc. | ProZ tries to identify components. So, it is recommended to use schema definitions instead of abbreviation definitions (\defs instead of ==) when defining state, initialisation, operations, etc. | ||
Line 93: | Line 92: | ||
E.g. ProZ checks if the square function in 2.3.a is a total function by enumerating it (it checks the function only for a limited interval). For more complex definitions the number of entries is often too large to check. | E.g. ProZ checks if the square function in 2.3.a is a total function by enumerating it (it checks the function only for a limited interval). For more complex definitions the number of entries is often too large to check. | ||
When the user is sure that those properties are satisfied (like in our example), a solution is relaxing the declaration from "square : Z -> Z" to "square : Z <-> Z". | When the user is sure that those properties are satisfied (like in our example), a solution is relaxing the declaration from "square : Z -> Z" to "square : Z <-> Z". | ||
Sometimes this is not easy to do, | Sometimes this is not easy to do, for instance if schema types are used which imply other constraints. | ||
ProZ supports an operation \prozignore that instructs ProZ to ignore all constraints on the type and to use just the underlying type. | ProZ supports an operation \prozignore that instructs ProZ to ignore all constraints on the type and to use just the underlying type. For example, the square function could be defined by: | ||
| square : \prozignore( Z -> Z ) | | square : \prozignore( Z -> Z ) | ||
Line 104: | Line 103: | ||
\newcommand{\prozignore}{ignore_\textsl{\tiny ProZ}} | \newcommand{\prozignore}{ignore_\textsl{\tiny ProZ}} | ||
You can change the definition of the macro as you like | You can change the definition of the macro as you like because the content is ignored by ProZ. Then you must introduce a generic definition of \prozignore. The definition is ignored by ProB, but Fuzz needs it for type checking. | ||
%%pregen \prozignore | %%pregen \prozignore | ||
Line 111: | Line 110: | ||
\end{gendef} | \end{gendef} | ||
It is also possible to append | It is also possible to append these lines to the "fuzzlib" in the fuzz distribution. | ||
=== Translation to B === | === Translation to B === | ||
You can inspect the result of the translation process with "Show internal representation" in the "Debug" menu. | You can inspect the result of the translation process with "Show internal representation" in the "Debug" menu. | ||
Please note | Please note that the shown B machine is normally not syntactically correct because of | ||
* additional constructs like free types | * additional constructs like free types | ||
* additional type information of the form "var:type" | * additional type information of the form "var:type" | ||
* names with primes (') or question marks, etc. | * names with primes (') or question marks, etc. | ||
* the pretty printer | * lack of support from the pretty printer for every construct | ||
== Known Limitations == | == Known Limitations == |
ProZ is a extension of the ProB animator and model checker to support Z specifications. It uses the Fuzz Type Checker by Mike Spivey for extracting the formal specification from a LaTeX file. On the website you can also find documentation about the syntax of Z specifications.
A Z specification frequently makes use of comprehension sets, which are often introduced by the underlying translation process from Z to B. Normally those comprehension sets should be treated symbolically. To support this, you should set the following in the preferences menu:
Animation Preferences -> - Lazy expansion of lambdas & set comprehensions: True - Convert lazy form back into explicit form for Variables and Constants: False
To identify the components (like state, initialisation, operations) of a Z specification, ProZ expects a certain structure of the specification: There must be a schema called "Init". "Init" describes the initialisation of the state. "Init" must include exactly one schema in the declaration part. This schema is assumed to be the state schema.
For example, let S be the state schema (= is used for \defs):
S = [ x,y:N ]
There are two supported styles for the initialisation:
a) Init = [ S | x=0 /\ y=1] b) Init = [ S'| x'=0 /\ y'=1 ]
If you want to use the logic of other schemas besides the state schema in the initialisation, you can do that by including those schemas in the predicate part.
ProZ identifies schemas as operations if they satisfy the following properties:
Example: Let S be defined as above:
A = [ \Delta S | x'=x+1 /\ y'=y ] B = [ x,y,x',y':N | x'=x+1 /\ y'=y ] C = [ x,x':N | x'=x+1 ] D = [ y,y':N | y'=y ] E = C /\ D F = [ \Xi S | x=0 ]
Then the schemas A,B and E describe all the same operation. F is also identified as an operation that leaves the state unchanged.
If axiomatic definitions are present, the declared variables are treated like constants. In the first step of the animation, ProB searches for values that satisfy all predicates of the axiomatic definitions are searched. After the first step, the predicates of the axiomatic definitions are ignored. If you want to define functions in an axiomatic definition, consider that ProB can treat lambda expressions and set comprehensions symbolically. Example: The definition of a function "square" could be
a)
| square : Z -> Z |----------------------- | square = (\lambda x:Z @ x*x)
b)
| square : Z -> Z |----------------------- | \forall x:Z @ square x = x*x
When using ProZ, it is preferable to use the method "a" because the lambda expression can be interpreted symbolically. If "b" is used, ProB will try to find a explicit set that will satisfy the given property.
You can add a B-style invariant to the specification by defining a schema "Invariant" that declares a subset of the state variables. In each explored state the invariant will be checked. The model checking feature of ProB will try to find states that violate the invariant.
It is possible to limit the search space of the model checker by adding a schema "Scope" that declares a subset of the state variables. If such a schema is present, each explored state is checked, if it satisfies the predicate. If not, the state is not further explored.
Abbreviation definitions (e.g. Abbr == {1,2,3}) are used like macros by ProZ. A reference to an abbreviation is replaced by its definition in a preprocessor phase. Thereby schemas defined by abbreviation definitions are ignored when ProZ tries to identify components. So, it is recommended to use schema definitions instead of abbreviation definitions (\defs instead of ==) when defining state, initialisation, operations, etc.
Sometimes it is not desired to check properties of some variables. E.g. ProZ checks if the square function in 2.3.a is a total function by enumerating it (it checks the function only for a limited interval). For more complex definitions the number of entries is often too large to check. When the user is sure that those properties are satisfied (like in our example), a solution is relaxing the declaration from "square : Z -> Z" to "square : Z <-> Z". Sometimes this is not easy to do, for instance if schema types are used which imply other constraints.
ProZ supports an operation \prozignore that instructs ProZ to ignore all constraints on the type and to use just the underlying type. For example, the square function could be defined by:
| square : \prozignore( Z -> Z ) |----------------------- | square = (\lambda x:Z @ x*x)
If you want to use \prozignore, you must first define a TeX command \prozignore:
\newcommand{\prozignore}{ignore_\textsl{\tiny ProZ}}
You can change the definition of the macro as you like because the content is ignored by ProZ. Then you must introduce a generic definition of \prozignore. The definition is ignored by ProB, but Fuzz needs it for type checking.
%%pregen \prozignore \begin{gendef}[X] \prozignore~\_ : \power X \end{gendef}
It is also possible to append these lines to the "fuzzlib" in the fuzz distribution.
You can inspect the result of the translation process with "Show internal representation" in the "Debug" menu. Please note that the shown B machine is normally not syntactically correct because of