Skip to content
Snippets Groups Projects
Commit 01632242 authored by dgelessus's avatar dgelessus
Browse files

Remove OtherLanguages section whose content can be found on the wiki

parent 539f0cdc
Branches
No related tags found
No related merge requests found
[[proz]]
= ProZ
ProZ is a extension
of the ProB animator and model checker to support Z specifications. It
uses the http://spivey.oriel.ox.ac.uk/mike/fuzz[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. The
https://www3.hhu.de/stups/downloads/pdf/proz07.pdf[iFM'07
article on ProZ] contains more details about the implementation.
[[preferences-for-proz]]
== Preferences
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
....
[[structure-of-the-z-specification]]
== Structure of the Z Specification
[[state-and-initialization]]
=== State and Initialization
To identify the components (like state, initialization, operations) of a
Z specification, ProZ expects a certain structure of the specification:
There must be a schema called "Init". "Init" describes the
initialization 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 initialization:
....
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 initialization, you can do that by including those schemas in the
predicate part.
[[operations]]
==== Operations
ProZ identifies schemas as operations if they satisfy the following
properties:
* All variables of the state and their primed counterpart are declared
in the operation. Usually this is done by including "\Delta S" in the
operation (with S being the state schema).
* The operation is not referenced by any other schema in the
specification
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.
[[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. 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.
[[invariant]]
==== Invariant
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.
[[scope-proz]]
==== Scope
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]]
==== Abbreviation Definitions
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, initialization,
operations, etc.
[[graphical-animation-proz]]
=== Graphical animation
(*Please note that this functionality is part of the next version. If
you want to use graphical animation, please download a version from the
<<download,Nightly build>>.*)
Analogous to the graphical animation for B specifications, you can
define a function that maps a coordinate to an image. Then ProZ will
display the grid of images while animating the specification.
To use this feature, add a schema *Proz_Settings* that contains a
variable *animation_function*. The animation function should map a
coordinate to an image. A coordinate is a pair of numbers or given sets.
The type used for images must be an enumerated set where the names of
the elements denote their file names (without the suffix .gif).
Please see the specification *jars.tex* which is bundled with the ProB
Tcl/Tk version for <<download,Download>> (inside the
examples/Z/GraphicalAnimation/ directory). This is the part of the
specification that defines the animation function (actually it defines a
pair of animation functions: the default function over which the other
function is overlaid; see
<<graphical-visualization,Graphical_Visualization>> for more
details):
....
We declare a type for the used images, the names of the elements refer to the file names of the GIF files.
\begin{zed}
Images ::= Filled | Empty | Void
\end{zed}
The animation consists of a grid of images that is updated in each new state.
The $animation_function$ maps a coordinate to an image where $(1\mapsto 1)$ is the upper-left corner.
\begin{schema}{ProZ_Settings}
Level \\
animation_function_default : (\nat \cross Jars) \pfun Images \\
animation_function : (\nat \cross Jars) \pfun Images \\
\where
animation_function_default = (1\upto global_maximum \cross Jars) \cross \{ Void \} \\
animation_function = \\
\t1 (\{ l:1\upto global_maximum; c:Jars | l\leq max_fill~c @ \\
\t2 global_maximum+1-l\mapsto c\} \cross \{Empty\}) \oplus \\
\t1 (\{ l:1\upto global_maximum; c:Jars | l\leq level~c @ \\
\t2 global_maximum+1-l\mapsto c\} \cross \{Filled\})
\end{schema}
....
Here is how the animation of the specification should look like:
image::ProZ_jars.png[]
[[special-constructs]]
=== Special constructs
[[prozignore]]
==== prozignore
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.
[[translation-to-b]]
==== Translation to B
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
* additional constructs like free types
* additional type information of the form "var:type"
* names with primes (') or question marks, etc.
* lack of support from the pretty printer for every construct
[[known-limitations]]
=== Known Limitations
* Generic definitions are not supported yet.
* Miscellaneous unsupported constructs
** reflexive-transitive closure
** probably other?
* The error messages are not very helpful yet.
[[summary-of-supported-operators]]
=== Summary of Supported Operators
....
== Logical predicates:
P \land Q conjunction
P \lor Q disjunction
P \implies Q implication
P \iff Q equivalence
\lnot P negation
== Quantifiers:
\forall x:T | P @ Q universal quantification (P => Q)
\exists x:T | P @ Q existential quantification (P & Q)
\exists_1 x:T | P @ Q exactly one existential quantification
== Sets:
\emptyset empty set
\{E,F\} set extension
\{~x:S | P~\} set comprehension
E \in S element of
E \notin S not element of
S \cup T union
S \cap T intersection
S \setminus T set difference
\power S power set
\# S cardinality
S \subseteq T subset predicate
S \subset T strict subset
\bigcup A generalized union of sets of sets
\bigcap A generalized intersection of sets of sets
== Pairs:
E \mapsto F pair
S \cross T Cartesian product
first E first part of pair
second E second part of pair
== Numbers:
\nat Natural numbers
\num Integers
\nat_1 Positive natural numbers
m < n less
m \leq n less equal
m > n greater
m \geq n greater equal
m + n addition
m - n difference
m * n multiplication
m \div n division
m \mod n modulo**
m \upto n m..n
min S minimum of a set
max S maximum of a set
succ n successor of a number
**: modulo of negative numbers not supported
== Functions:
S \rel T relations
S \pfun T partial functions from S to T
S \fun T total functions from S to T
S \pinj T partial injections from S to T
S \inj T total injections from S to T
S \bij T total bijections from S to T
\dom R domain
\ran R range
\id S identity relation over S
S \dres R domain restriction
S \ndres R domain anti-restriction
R \rres S range restriction
R \nrres S range anti-restriction
R \oplus Q overriding
R \plus transitive closure
== Sequences:
\langle E,... \rangle explicit sequence
\seq S sequences over S
\seq_1 S non-empty sequences
\iseq S injective sequences over S
rev E reverse a sequence
head E first element of a sequence
last E last element of a sequence
tail E sequence with first element removed
front E all but the last element
E \cat F concatenation of two sequences
\dcat ss concatenation of sequences of sequences
E \filter F subsequence of elements of sequence E contained in set F
E \extract F extract subsequence from F with indexes in set E
squash F compaction
E \prefix F sequence E is a prefix of F
E \suffix F sequence E is a suffix of F
E \inseq F E is a sequence occuring in the middle of F (segment relation)
\disjoint E family of sets E is disjoint
E \partition F family of sets E is a partition of set F
Bags:
----------
\bag S bags over S
\lbag E,... \rbag explicit bag
count B E count of occurences of E in bag B
B \bcount E infix version of count
E \inbag B bag membership
B \subbageq C sub-bag relation
B \uplus C bag union
B \uminus C bag difference
items E bag of items in a sequence
n \otimes B bag scaling
Other:
-----------
\IF P \THEN E \ELSE F if-then-else expression
(\LET x == E @ F) Let-expression
....
[[tla]]
= TLA
As of version 1.3.5, ProB supports
http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+].
[[using-prob-for-animation-and-model-checking-of-tla-specifications]]
== Using ProB for Animation and Model Checking of TLA+ specifications
The http://nightly.cobra.cs.uni-duesseldorf.de/tcl/[latest version of
ProB] uses the translator TLA2B, which translates the non temporal part
of a
http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+]
module to a B machine. To use ProB for TLA+ you have to download the TLA
tools. They are released as an open source project, under the
http://research.microsoft.com/en-us/um/people/lamport/tla/license.html[MIT
License]. In the ProB Tcl/Tk GUI you have to select the menu command
"Download and Install TLA Tools" in the Help menu.
image::Download_TLA_Tools.png[]
When you open a TLA+ module ProB generates the translated B machine in
the same folder and loads it in the background. If there is a valid
translation you can animate and model check the TLA+ specification.
There are many working examples in the 'ProB/Examples/TLA+/'-directory.
There is also an
https://www3.hhu.de/stups/downloads/pdf/HansenLeuschelTLA2012.pdf[iFM'2012
paper] that describes our approach and performs some comparison with
TLC. Our <<prob-logic-calculator,online ProB Logic Calculator>> now
also supports TLA syntax and you can experiment with its predicate and
expression evaluation capabilities.
[[tla2b]]
== TLA2B
The parser and semantic analyzer
http://research.microsoft.com/en-us/um/people/lamport/tla/sany.html[SANY]
serves as the front end of TLA2B. SANY was written by Jean-Charles
Grégoire and David Jefferson and is also the front end of the model
checker
http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html[TLC].
After parsing there is type checking phase, in which types of variables
and constants are inferred. So there is no need to especially declare
types in a invariant clause (in the manner of the B method). Moreover it
checks if a TLA+ module is translatable (see Limitations of
Translation).
To tell TLA2B the name of a specification of a TLA+ module you can use a
configuration file, just like for TLC. The configuration file must have
the same name as the name of the module and the filename extension
'cfg'. The configuration file parser is the same as for TLC so you can
look up the syntax in the
http://research.microsoft.com/en-us/um/people/lamport/tla/book.html['Specifying
Systems'-book] (Leslie Lamport). If there is no configuration file
available TLA2B looks for a TLA+ definition named 'Spec' or
alternatively for a 'Init' and a 'Next' definition describing the
initial state and the next state relation. Besides that in the
configuration file you can give a constant a value but this is not
mandatory, in contrast to TLC. Otherwise ProB lets you choose during the
animation process a value for the constant which satisfy the assumptions
under the ASSUME clause. TLA2B supports furthermore overriding of a
constant or definition by another definition in the configuration file.
[[supported-tla-syntax]]
== Supported TLA+ syntax
....
Logic
-----
P /\ Q conjunction
P \/ Q disjunction
~ or \lnot or \neg negation
=> implication
<=> or \equiv equivalence
TRUE
FALSE
BOOLEAN set containing TRUE and FALSE
\A x \in S : P universal quantification
\E x \in S : P existential quantification
Equality:
------
e = f equality
e # f or e /= f inequality
Sets
------
{d, e} set consisting of elements d, e
{x \in S : P} set of elements x in S satisfying p
{e : x \in S} set of elements e such that x in S
e \in S element of
e \notin S not element of
S \cup T or S \union T set union
S \cap T or S \intersect set intersection
S \subseteq T equality or subset of
S \ t set difference
SUBSET S set of subsets of S
UNION S union of all elements of S
Functions
------
f[e] function application
DOMAIN f domain of function f
[x \in S |-> e] function f such that f[x] = e for x in S
[S -> T] Set of functions f with f[x] in T for x in S
[f EXCEPT ![e] = d] the function equal to f except f[e] = d
Records
-------
r.id the id-field of record r
[id_1|->e_1,...,id_n|->e_n] construct a record with given field names and values
[id_1:S_1,...,id_n:S_n] set of records with given fields and field types
[r EXCEPT !.id = e] the record equal to r except r.id = e
Strings and Numbers
-------------------
"abc" a string
STRING set of a strings
123 a number
Miscellaneous constructs
------------------------
IF P THEN e_1 ELSE e_2
CASE P_1 -> e_1 [] ... [] P_n ->e_n
CASE P_1 -> e_1 [] ... [] P_n ->e_n [] OTHER -> e
LET d_1 == e_1 ... d_n == e_n IN e
Action Operators
----------------
v' prime operator (only variables are able to be primed)
UNCHANGED v v'=v
UNCHANGED <<v_1, v_2>> v_1'=v_1 /\ v_2=v_2
Supported standard modules
--------------------------
Naturals
--------
x + y addition
x - y difference
x * y multiplication
x \div y division
x % y remainder of division
x ^ y exponentiation
x > y greater than
x < y less than
x \geq y greater than or equal
x \leq y less than or equal
x .. y set of numbers from x to y
Nat set of natural numbers
Integers
--------
-x unary minus
Int set of integers
Sequences
---------
SubSeq(s,m,n) subsequence of s from component m to n
Append(s, e) appending e to sequence s
Len(s) length of sequence s
Seq(s) set of sequences
s_1 \o s_2 or s_1 \circ s_2 concatenation of s_1 and s_2
Head(s)
Tail(s)
FiniteSets
----------
Cardinality(S)
IsFiniteSet(S) (ProB can only handle certain infinite sets as argument)
typical structure of a TLA+ module
--------------------------
---- MODULE m ----
EXTENDS m_1, m_2
CONSTANTS c_1, c_2
ASSUME c_1 = ...
VARIABLES v_1, v_2
foo == ...
Init == ...
Next == ...
Spec == ...
====================
....
Temporal formulas and unused definitions are ignored by TLA2B (they are
also ignored by the type inference algorithm).
[[limitations-of-the-translation]]
== Limitations of the translation
* due to the strict type system of the B method there are several
restrictions to TLA+ modules.
** the elements of a set must have the same type (domain and range of a
function are sets)
** TLA+ tuples are translated as sequences in B, hence all components of
the tuple must have the same type
* TLA2B do not support 2nd-order operators, i.e. operators that take a
operator with arguments as argument (e.g.: `foo(bar(_),p)`)
[[tla-actions]]
== TLA+ Actions
'''''
TLA2B divides the next state relation into different actions if a
disjunction occurs. IF a existential quantification occurs TLA2B
searches for further actions in the predicate of the quantification and
adds the bounded variables as arguments to these actions. IF a
definition call occurs and the definition has no arguments TLA2B goes
into the definition searching for further actions. The displayed actions
by ProB are not necessarily identical with the actions determined by
TLC.
[[understanding-the-type-checker]]
== Understanding the type checker
Corresponding B types to TLA+ data values (let type(e) be the type of
the expression e):
....
TLA+ data B Type
--------------------------------------------------
number e.g. 123 INTEGER
string e.g. "abc" STRING
bool value e.g. TRUE BOOL
set e.g. {e,f} POW(type(e)), type(e) = type(f)
function e.g. [x \in S |-> e] POW(type(x)*type(e)), type(S) = POW(type(x))
sequence e.g. <<a,b>> POW(INTEGER*type(a)), type(a) = type(b)
record e.g. [id_1|->e_1,...,id_n|->e_n] struct(id_1:type(e_1),...,id_n:type(e_n))
model value ENUM
(only definable in config file)
Nat POW(INTEGER)
Int POW(INTEGER)
STRING POW(STRING)
BOOLEAN POW(BOOL)
SUBSET S POW(type(S))
....
You can only compare data values with the same type.
:leveloffset: -1
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment