(73 intermediate revisions by 3 users not shown) | |||
Line 4: | Line 4: | ||
== Summary of B Syntax == | == Summary of B Syntax == | ||
Below we describe the "classical" B syntax as supported by ProB. | |||
You may also wish to consult | |||
* The B summary by Ken Robinson ([[File:B-summary.pdf|PDF File]]) | |||
* The [https://www.atelierb.eu Atelier-B] reference manual ([https://www.atelierb.eu/wp-content/uploads/2023/10/b-language-reference-manual.pdf b-language-reference-manual.pdf]) | |||
=== Logical predicates === | |||
=== Logical predicates | |||
<pre> | <pre> | ||
P & Q | P & Q conjunction | ||
P or Q | P or Q disjunction | ||
P => Q | P => Q implication | ||
P <=> Q | P <=> Q equivalence | ||
not P negation | not(P) negation | ||
!(x).(P=>Q) universal quantification | !(x).(P=>Q) universal quantification | ||
#(x).(P&Q) | #(x).(P&Q) existential quantification | ||
btrue truth (this is a predicate) | |||
bfalse falsity (this is a predicate) | |||
</pre> | </pre> | ||
Line 20: | Line 25: | ||
Note: you can also introduce multiple variables inside a universal or existential quantification, e.g., <tt>!(x,y).(P => Q)</tt>. | Note: you can also introduce multiple variables inside a universal or existential quantification, e.g., <tt>!(x,y).(P => Q)</tt>. | ||
=== Equality | === Equality === | ||
<pre> | <pre> | ||
E = F | E = F equality | ||
E /= F | E /= F disequality | ||
</pre> | </pre> | ||
=== Booleans | === Booleans === | ||
<pre> | <pre> | ||
TRUE | TRUE truth value (this is an expression) | ||
FALSE | FALSE falsity value (this is an expression) | ||
BOOL | BOOL set of boolean values ({TRUE,FALSE}) | ||
bool(P) | bool(P) convert predicate into BOOL value | ||
</pre> | </pre> | ||
Warning: <tt>TRUE</tt> and <tt>FALSE</tt> are values and <em>not</em> predicates in B and cannot be combined using logical connectives. | Warning: <tt>TRUE</tt> and <tt>FALSE</tt> are expression values and <em>not</em> predicates in B and cannot be combined using logical connectives. | ||
To combine two boolean values <tt>x</tt> and <tt>y</tt> using conjunction you have to write <tt>x=TRUE & y=TRUE</tt>. | To combine two boolean values <tt>x</tt> and <tt>y</tt> using conjunction you have to write <tt>x=TRUE & y=TRUE</tt>. | ||
To convert a predicate such as <tt>z>0</tt> into a boolean value you have to use <tt>bool(z>0)</tt>. | To convert a predicate such as <tt>z>0</tt> into a boolean value you have to use <tt>bool(z>0)</tt>. | ||
=== Sets | === Sets === | ||
<pre> | <pre> | ||
{} | {} empty set | ||
{E} | {E} singleton set | ||
{E,F} | {E,F} set enumeration | ||
{x|P} comprehension set | {x|P} comprehension set | ||
POW(S) | {(x).P|E} Event-B style comprehension set (brackets needed) | ||
POW1(S) | POW(S) power set | ||
FIN(S) | POW1(S) set of non-empty subsets | ||
FIN1(S) | FIN(S) set of all finite subsets | ||
card(S) | FIN1(S) set of all non-empty finite subsets | ||
S*T | card(S) cardinality | ||
S\/T | S*T cartesian product | ||
S/\T | S\/T set union | ||
S-T | S/\T set intersection | ||
E:S | S-T or S \ T set difference | ||
E/:S | E:S element of | ||
S<:T | E/:S not element of | ||
S/<:T | S<:T subset of | ||
S<<:T | S/<:T not subset of | ||
S/<<:T | S<<:T strict subset of | ||
S/<<:T not strict subset of | |||
union(S) generalised union over sets of sets | union(S) generalised union over sets of sets | ||
inter(S) | inter(S) generalised intersection over sets of sets | ||
UNION(z).(P|E) generalised union with predicate | UNION(z).(P|E) generalised union with predicate | ||
INTER(z).(P|E) generalised intersection with predicate | INTER(z).(P|E) generalised intersection with predicate | ||
</pre> | </pre> | ||
=== | === Integers === | ||
<pre> | <pre> | ||
INTEGER | INTEGER set of integers | ||
NATURAL | NATURAL set of natural numbers | ||
NATURAL1 | NATURAL1 set of non-zero natural numbers | ||
INT | INT set of implementable integers (MININT..MAXINT) | ||
NAT | NAT set of implementable natural numbers | ||
NAT1 | NAT1 set of non-zero implementable natural numbers | ||
n..m | n..m set of numbers from n to m | ||
MININT | MININT the minimum implementable integer | ||
MAXINT | MAXINT the maximum implementable integer | ||
m>n | m>n greater than | ||
m<n | m<n less than | ||
m>=n | m>=n greater than or equal | ||
m<=n | m<=n less than or equal | ||
max(S) | max(S) maximum of a set of numbers | ||
min(S) | min(S) minimum of a set of numbers | ||
m+n | m+n addition | ||
m-n | m-n difference | ||
m*n | m*n multiplication | ||
m/n | m/n division | ||
m**n | m**n power | ||
m mod n | m mod n remainder of division | ||
PI(z).(P|E) | PI(z).(P|E) set product | ||
SIGMA(z).(P|E) | SIGMA(z).(P|E) set summation | ||
succ(n) | succ(n) successor (n+1) | ||
pred(n) | pred(n) predecessor (n-1) | ||
0xH | 0xH hexadecimal literal, where H is a sequence of letters in [0-9A-Fa-f] | ||
</pre> | </pre> | ||
=== Relations | === Relations === | ||
<pre> | <pre> | ||
S<->T | S<->T relation | ||
S<<->T | S<<->T total relation | ||
S<->>T | S<->>T surjective relation | ||
S<<->>T | S<<->>T total surjective relation | ||
E|->F | E|->F maplet | ||
dom(r) | dom(r) domain of relation | ||
ran(r) | ran(r) range of relation | ||
id(S) | id(S) identity relation | ||
S<|r | S<|r domain restriction | ||
S<<|r | S<<|r domain subtraction | ||
r|>S | r|>S range restriction | ||
r|>>S | r|>>S range subtraction | ||
r~ | r~ inverse of relation | ||
r[S] | r[S] relational image | ||
r1<+r2 | r1<+r2 relational overriding (r2 overrides r1) | ||
r1><r2 | r1><r2 direct product (all pairs (x,(y,z)) with x,y:r1 and x,z:r2) | ||
(r1;r2) | (r1;r2) relational composition {x,y| x|->z:r1 & z|->y:r2} | ||
(r1||r2) | (r1||r2) parallel product (all pairs ((x,v),(y,w)) with x,y:r1 and v,w:r2) | ||
prj1(S,T) projection function (usage prj1(Dom,Ran)(Pair)) | prj1(S,T) projection function (usage prj1(Dom,Ran)(Pair)) | ||
prj2(S,T) projection function (usage prj2(Dom,Ran)(Pair)) | prj2(S,T) projection function (usage prj2(Dom,Ran)(Pair)) | ||
prj1(Pair) and prj2(Pair) are also allowed | |||
fnc(r) translate relation A<->B into function A+->POW(B) | |||
rel(r) translate relation A<->POW(B) into relation A<->B | |||
closure1(r) transitive closure | closure1(r) transitive closure | ||
closure(r) reflexive & transitive closure | closure(r) reflexive & transitive closure | ||
( | (equal to id(TYPEOF_r) \/ closure1(r)) | ||
iterate(r,n) iteration of r with n>=0 | iterate(r,n) iteration of r with n>=0 | ||
(Note: iterate(r,0) = id(s) where s = | (Note: iterate(r,0)=id(s) where s=TYPEOF_r) | ||
</pre> | </pre> | ||
=== Functions | === Functions === | ||
<pre> | <pre> | ||
S+->T partial function | |||
S-->T total function | |||
S+->>T partial surjection | |||
S-->>T total surjection | |||
S>+>T partial injection | |||
S>->T total injection | |||
S>+>>T partial bijection | |||
S>->>T total bijection | |||
%x.(P|E) lambda abstraction | |||
f(E) function application | |||
f(E1,...,En) is also supported (as well as f(E1|->E2...|->En)) | |||
</pre> | </pre> | ||
=== Sequences | === Sequences === | ||
<pre> | <pre> | ||
[] or <> empty sequence | |||
[E] singleton sequence | |||
[E,F] constructed sequence | |||
seq(S) set of sequences over S | |||
seq1(S) set of non-empty sequences over S | |||
iseq(S) set of injective sequences over S | |||
iseq1(S) set of non-empty injective sequences over S | |||
perm(S) set of bijective sequences (permutations) over S | |||
size(s) size of sequence | |||
s^t concatenation | |||
E->s prepend element | |||
s<-E append element | |||
rev(s) reverse of sequence | |||
first(s) first element | |||
last(s) last element | |||
front(s) front of sequence (all but last element) | |||
tail(s) tail of sequence (all but first element) | |||
conc(S) concatenation of sequence of sequences | |||
s/|\n take first n elements of sequence | |||
s\|/n drop first n elements from sequence | |||
</pre> | </pre> | ||
=== Records | === Records === | ||
<pre> | <pre> | ||
struct(ID:S,...,ID:S) set of records with given fields and field types | |||
rec(ID:E,...,ID:E) construct a record with given field names and values | |||
E'ID get value of field with name ID | |||
</pre> | </pre> | ||
=== | === Identifiers === | ||
<pre> | <pre> | ||
ID must start with letter (ASCII or Unicode), can then contain | |||
letters (ASCII or Unicode), digits and underscore (_) and | |||
can end with Unicode subscripts followed by Unicode primes | |||
M.ID composed identifier for identifier coming from included machine M | |||
`ID` an identifier in backquotes can contain almost any character (except newline) | |||
</pre> | |||
=== Strings === | |||
<pre> | |||
"astring" a specific (single-line) string value | |||
'''astring''' an alternate way of writing (multi-line) strings, no need to escape " | |||
```tstring``` template strings, where ${Expr} parts are evaluated and converted to string, | |||
you can provide options separated by commas in square brackets like $[2f]{Expr}. | |||
Valid options are: Nf (for floats/reals), Nd (for integer), Np (padding), | |||
ascii (can be abbreviated to a), unicode (can be abbreviated to u). | |||
STRING the set of all strings | |||
</pre> | </pre> | ||
Atelier-B does not support any operations on strings, apart from equality and disequality. | Atelier-B does not support any operations on strings, apart from equality and disequality. | ||
In ProB, however, some of the sequence operators work also on strings: | |||
<pre> | |||
size(s) the length of a string s | |||
rev(s) the reverse of a string s | |||
s ^ t the concatenation of two strings | |||
conc(ss) the concatenation of a sequence of strings | |||
</pre> | |||
You can turn this support off using the <tt>STRING_AS_SEQUENCE</tt> preference. | |||
The [[External_Functions|library]] LibraryStrings.def in stdlib contains additional useful external functions | |||
(like <tt>TO_STRING</tt>, <tt>STRING_SPLIT</tt>, <tt>FORMAT_TO_STRING</tt>, <tt>INT_TO_HEX_STRING</tt>, ...). | |||
ProB also allows multi-line strings. | |||
As of version 1.7.0, ProB will support the following escape sequences within strings: | As of version 1.7.0, ProB will support the following escape sequences within strings: | ||
\n | <pre> | ||
\r | \n newline (ASCII character 13) | ||
\r carriage return (ASCII 10) | |||
\t tab (ASCII 9) | \t tab (ASCII 9) | ||
\" | \" the double quote symbol " | ||
\' | \' the single quote symbol ' | ||
\\ | \\ the backslash symbol | ||
</pre> | |||
Within single-line string literals, you do not need to escape <tt>'</tt>. | |||
Within multi-line string literals, you do not need to escape <tt>"</tt> and you can use | |||
tabs and newlines. | |||
ProB assumes that all B machines and strings use the UTF-8 encoding. | ProB assumes that all B machines and strings use the UTF-8 encoding. | ||
=== Reals === | |||
=== Reals | |||
<pre> | <pre> | ||
REAL set of reals | REAL set of reals | ||
FLOAT set of floating point numbers | FLOAT set of floating point numbers | ||
i.f real literal, where i and f are | i.f real literal in decimal notation, where i and f are natural numbers | ||
i.fEg real literal in scientific notation, where i,f are natural numbers and g is an integer | |||
real(n) convert an integer n into a real number | real(n) convert an integer n into a real number | ||
floor(r) convert a real r | floor(r) convert a real r into an integer | ||
ceiling(r) convert a real r | ceiling(r) convert a real r into an integer | ||
</pre> | </pre> | ||
One can also use a lowercase <tt>e</tt> for literals in scientific notation (e.g. <tt>1.0e-10</tt>). | |||
Standard arithmetic operators can be applied to reals: +, - , *, /, SIGMA, PI. | Standard arithmetic operators can be applied to reals: +, - , *, /, SIGMA, PI. | ||
Exponentiation of a real with an integer is also allowed. | Exponentiation of a real with an integer is also allowed. | ||
Line 225: | Line 247: | ||
is also not stable yet. Currently ProB supports floating point numbers only. | is also not stable yet. Currently ProB supports floating point numbers only. | ||
Warning: properties such as associativity and commutativity of arithmetic operators | Warning: properties such as associativity and commutativity of arithmetic operators | ||
thus | thus do not hold. | ||
The library LibraryReals.def in stdlib contains additional useful external functions | The [[External_Functions|library]] LibraryReals.def in stdlib contains additional useful external functions | ||
(like RSIN, RCOS, RLOG, RSQRT, RPOW, ...). | (like <tt>RSIN</tt>, <tt>RCOS</tt>, <tt>RLOG</tt>, <tt>RSQRT</tt>, <tt>RPOW</tt>, ...). | ||
You can turn off support for REALS using the preference ALLOW_REALS. | You can turn off support for REALS using the preference <tt>ALLOW_REALS</tt>. | ||
The <tt>REAL_SOLVER</tt> preference how constraints are solved. | |||
=== Trees | === Trees === | ||
Nodes in the tree are denoted by index sequences (branches), e.g, n=[1,2,1] | Nodes in the tree are denoted by index sequences (branches), e.g, <tt>n=[1,2,1]</tt> | ||
Each node in the tree is labelled with an element from a domain S | Each node in the tree is labelled with an element from a domain S. | ||
A tree is a function mapping of branches to elements of the domain S. | A tree is a function mapping of branches to elements of the domain S. | ||
<pre> | <pre> | ||
tree(S) set of trees over domain S | |||
btree(S) set of binary trees over domain S | |||
top(t) top of a tree | |||
const(E,s) construct a tree from info E and sequence of subtrees s | |||
rank(t,n) rank of the node at end of branch n in the tree t | |||
father(t,n) father of the node denoted by branch n in the tree t | |||
son(t,n,i) the ith son of the node denoted by branch n in tree t | |||
sons(t) the sequence of sons of the root of the tree t | |||
subtree(t,n) | |||
arity(t,n) | |||
bin(E) construct a binary tree with a single node E | |||
bin(tl,E,tr) construct a binary tree with root info E and subtrees tl,tr | |||
left(t) the left (first) son of the root of the binary tree t | |||
right(t) the right (last) son of the root of the binary tree t | |||
sizet(t) the size of the tree (number of nodes) | |||
prefix(t) the nodes of the tree t in prefix order | |||
postfix(t) the nodes of the tree t in prefix order | |||
mirror, infix are recognised by the parser but not yet supported by ProB itself | |||
</pre> | </pre> | ||
=== LET and IF-THEN-ELSE === | === LET and IF-THEN-ELSE === | ||
ProB allows the following for predicates and | ProB allows the following for predicates, expressions and substitutions: | ||
<pre> | <pre> | ||
IF P THEN E1 END conditional branching | |||
IF P THEN E1 ELSIF E2 END we also allow multiple ELSIF branches | |||
IF P THEN E1 ELSE E2 END but you always need an ELSE branch for expressions and predicates | |||
IF P THEN E1 ELSIF E2 ELSE E3 END | |||
LET x1,... BE x1=E1 & ... IN E END introduce local variables | |||
</pre> | </pre> | ||
Note: the | Note: the expression <tt>Ei</tt> defining <tt>xi</tt> is allowed to use <tt>x1,...,x(i-1)</tt> for predicates/expressions. | ||
By setting the preference <tt>ALLOW_COMPLEX_LETS</tt> to <tt>TRUE</tt>, this is also allowed for substitutions. | |||
=== Statements (aka Substitutions) | === Statements (aka Substitutions) === | ||
<pre> | <pre> | ||
skip no operation | |||
x := E assignment | |||
f(x) := E functional override | |||
x :: S choice from set | |||
x : (P) choice by predicate P (constraining x; previous value of x is x$0) | |||
x <-- OP(x) call operation and assign return value | |||
G||H parallel substitution** | |||
G;H sequential composition** | |||
ANY x,... WHERE P THEN G END non deterministic choice | |||
LET x,... BE x=E & ... IN G END | |||
VAR x,... IN G END generate local variables | |||
PRE P THEN G END | |||
ASSERT P THEN G END | |||
CHOICE G OR H END | |||
IF P THEN G END | |||
IF P THEN G ELSE H END | |||
IF P1 THEN G1 ELSIF P2 THEN G2 ... END | |||
IF P1 THEN G1 ELSIF P2 THEN G2 ... ELSE Gn END | |||
SELECT P THEN G WHEN ... WHEN Q THEN H END | |||
SELECT P THEN G WHEN ... WHEN Q THEN H ELSE I END | |||
CASE E OF EITHER m THEN G OR n THEN H ... END END | |||
CASE E OF EITHER m THEN G OR n THEN H ... ELSE I END END | |||
WHILE P1 DO G INVARIANT P2 VARIANT E END | |||
WHEN P THEN G END is a synonym for SELECT P THEN G END | |||
</pre> | </pre> | ||
**: cannot be used at the top-level of an operation, but needs to | |||
be wrapped inside a <tt>BEGIN END</tt> or another statement (to avoid | |||
confusion with the operators <tt>;</tt> and <tt>||</tt> on relations). | |||
=== Machine header | === Machine header === | ||
<pre> | <pre> | ||
MACHINE or REFINEMENT or IMPLEMENTATION | |||
</pre> | </pre> | ||
Note: machine parameters can either be SETS (if identifier is all upper-case) | |||
or scalars (i.e., integer, boolean or SET element; if identifier is not | |||
all upper-case; typing must be provided be CONSTRAINTS) | |||
You can also use MODEL or SYSTEM as a synonym for MACHINE, as well | |||
as EVENTS as a synonym for OPERATIONS. | |||
ProB also supports the ref keyword of Atelier-B for event refinement. | |||
=== Machine sections | === Machine sections === | ||
<pre> | <pre> | ||
CONSTRAINTS P (logical predicate) | |||
SETS S;T={e1,e2,...};... | |||
FREETYPES x=x1,x2(arg2),...;... | |||
CONSTANTS x,y,... | |||
CONCRETE_CONSTANTS cx,cy,... | |||
PROPERTIES P (logical predicate) | |||
DEFINITIONS m(x,...) == BODY;... | |||
VARIABLES x,y,... | |||
CONCRETE_VARIABLES cv,cw,... | |||
INVARIANT P (logical predicate) | |||
ASSERTIONS P;...;P (list of logical predicates separated by ;) | |||
INITIALISATION S (substitution) | |||
OPERATIONS O;... (operations) | |||
</pre> | </pre> | ||
=== Machine inclusion | === Machine inclusion === | ||
<pre> | <pre> | ||
USES list of machines | |||
INCLUDES list of machines | |||
SEES list of machines | |||
EXTENDS list of machines | |||
PROMOTES list of operations | |||
REFINES machine | |||
</pre> | </pre> | ||
Note: Refinement machines should express the operation preconditions in terms of their own variables. | Note: Refinement machines should express the operation preconditions in terms of their own variables. | ||
=== Definitions | === Definitions === | ||
<pre> | <pre> | ||
NAME1 == Expression; Definition without arguments | |||
NAME2(ID,...,ID) == E2; Definition with arguments | |||
"FILE.def"; Include definitions from file | |||
</pre> | </pre> | ||
There are a few | There are a few specific definitions which can be used to influence ProB: | ||
<pre> | |||
GOAL == P to define a custom Goal predicate for Model Checking | |||
(the Goal is also set by using "Advanced Find...") | |||
SCOPE == P to limit the search space to "interesting" nodes | |||
scope_SETNAME == n..n to define custom cardinality for set SETNAME | |||
scope_SETNAME == n equivalent to 1..n | |||
SET_PREF_MININT == n | |||
SET_PREF_MAXINT == n | |||
SET_PREF_MAX_INITIALISATIONS == n max. number of intialisations computed | |||
SET_PREF_MAX_OPERATIONS == n max. number of enablings per operation computed | |||
MAX_OPERATIONS_OPNAME == n max. number of enablings for the operation OPNAME | |||
SET_PREF_SYMBOLIC == TRUE/FALSE | |||
SET_PREF_TIME_OUT == n time out for operation computation in ms | |||
ASSERT_LTL... == "LTL Formula" using X,F,G,U,R LTL operators + | |||
Y,O,H,S Past-LTL operators + | |||
atomic propositions: e(OpName), [OpName], {BPredicate} | |||
HEURISTIC_FUNCTION == n in directed model-checking mode nodes with smalles value will be processed first | |||
</pre> | |||
The following definitions allow providing a custom state visualization (n can be empty or a number): | |||
<pre> | <pre> | ||
ANIMATION_FUNCTIONn == e a function (INT*INT) +-> INT or an INT | |||
ANIMATION_FUNCTION_DEFAULT == e a function (INT*INT) +-> INT or an INT | |||
instead of any INT above you can also use BOOL or any SET | |||
as a result you can also use STRING values, | |||
or even other values which are pretty printed | |||
ANIMATION_IMGn == "PATH to .gif" a path to a gif file | |||
ANIMATION_STRn == "sometext" a string without spaces; | |||
the result integer n will be rendered as a string | |||
ANIMATION_STR_JUSTIFY_LEFT == TRUE computes the longest string in the outputs and pads | |||
the other strings accordingly | |||
SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == n additional padding between images in pixels | |||
SET_PREF_TK_CUSTOM_STATE_VIEW_STRING_PADDING == n additional padding between text in pixels | |||
</pre> | </pre> | ||
The following definitions allow providing a custom state | The following definitions allow providing a [[Custom Graph|custom state graph]] (n can be empty or a number): | ||
<pre> | |||
CUSTOM_GRAPH_NODESn == e define a set of nodes to be shown, | |||
nodes can also be pairs (Node,Colour), triples (Node,Shape,Colour) or | |||
records or sets of records like | |||
rec(color:Colour, shape:Shape, style:Style, label:Label, value:Node, ...) | |||
Colours are strings of valid Dot/Tk colors (e.g., "maroon" or "red") | |||
Shapes are strings of valid Dot shapes (e.g., "rect" or "hexagon"), and | |||
Styles are valid Dot shape styles (e.g., "rounded" or "solid" or "dashed") | |||
CUSTOM_GRAPH_EDGESn == e define a relation to be shown as a graph | |||
edges can either be pairs (node1,node2) or triples (node1,Label,node2) | |||
where Label is either a Dot/Tk color or a string or value representing | |||
the label to be used for the edges | |||
</pre> | |||
In both cases e can also be a record which defines default dot attributes like | |||
color, shape, style and description, e.g.: | |||
<pre> | <pre> | ||
CUSTOM_GRAPH_NODES == rec(color:"blue", shape:"rect", style:"filled", nodes:e); | |||
CUSTOM_GRAPH_EDGES == rec(color:"red", style:"dotted", dir:"none", penwidth:2, edges:e) | |||
</pre> | </pre> | ||
Alternatively, the complete graph can be put into one definition using [[Custom_Graph|<code>CUSTOM_GRAPH</code>]]. | |||
You have to define a single CUSTOM_GRAPH definition of a record with global graph attributes | |||
(like rankdir or layout) and optionally with edges and nodes attributes (replacing | |||
CUSTOM_GRAPH_EDGES and CUSTOM_GRAPH_NODES respectively), e.g.: | |||
<pre> | <pre> | ||
CUSTOM_GRAPH == rec(layout:"circo", nodes:mynodes, edges:myedges) | |||
</pre> | </pre> | ||
You can now also use a single CUSTOM_GRAPH definition of a record with global graph attributes | |||
(like rankdir or layout) and optionally with edges and nodes attributes | |||
(replacing CUSTOM_GRAPH_EDGES and CUSTOM_GRAPH_NODES respectively), e.g.: | |||
<pre> | <pre> | ||
CUSTOM_GRAPH == rec(layout:"circo", nodes:mynodes, edges:myedges) | |||
</pre> | </pre> | ||
These DEFINITIONS affect VisB: | You can also provide <tt>SEQUENCE_CHART_opname</tt> definitions for [[Generating UML Sequence Charts|generating UML sequence charts]]. | ||
These DEFINITIONS affect [[VisB|VisB]]: | |||
<pre> | <pre> | ||
VISB_JSON_FILE == "PATH to .json" a path to a default VisB JSON file for visualisation; | |||
if it is "" an empty SVG will be created | |||
VISB_SVG_OBJECTSn == ... define a record or set of records for creating new SVG objects | |||
VISB_SVG_UPDATESn == ... define a record or set of records containing updates of SVG objects | |||
VISB_SVG_HOVERSn == ... define a record or set of records for VisB hover functions | |||
VISB_SVG_BOX == ... record with dimensions (height, width) of a default empty SVG | |||
VISB_SVG_CONTENTS == ... defines a string to be included into a created empty SVG file | |||
</pre> | </pre> | ||
Line 414: | Line 457: | ||
<pre> | <pre> | ||
B supports two styles of comments: | B supports two styles of comments: | ||
/* ... */ block comments | |||
// ... line comments | |||
</pre> | </pre> | ||
Line 421: | Line 464: | ||
The whitespace between @ and PRAGMA is optional. | The whitespace between @ and PRAGMA is optional. | ||
<pre> | <pre> | ||
/*@symbolic */ put before comprehension set, lambda, union or composition to instruct ProB | |||
to keep it symbolic and not try to compute it explicitly | |||
/*@label LBL */ associates a label LBL with the following predicate | |||
(LBL must be identifier or a string "....") | |||
/*@desc DESC */ associates a description DESC with the preceding predicate or | |||
introduced identifier (in VARIABLES, CONSTANTS,... section) | |||
There are three special descriptions: | |||
/*@desc memo*/ to be put after identifiers in the ABSTRACT_CONSTANTS section | |||
indicating that these functions should be memoized | |||
/*@desc expand*/ to be put after identifiers (in VARIABLES, CONSTANTS,... section) | |||
indicating that they should be expanded and not kept symbolically | |||
/*@desc prob-ignore */ to be put after predicates (e.g., in PROPERTIES) which | |||
should be ignored by ProB | |||
when the preference USE_IGNORE_PRAGMAS is TRUE | |||
/*@file PATH */ associates a file for machines in SEES, INCLUDES, ... | |||
put pragma after a seen or included machine | |||
/*@package NAME */ at start of machine, machine file should be in folder NAME/... | |||
NAME can be qualified N1.N2...Nk, in which case the machine | |||
file should be in N1/N2/.../Nk | |||
/*@import-package NAME */ adds ../NAME to search paths for SEES,... | |||
NAME can also be qualified N1.N2...Nk, use after package pragma | |||
/*@generated */ can be put at the top of a machine file; indicates the machine | |||
is generated from some other source | |||
</pre> | </pre> | ||
=== File Extensions === | === File Extensions === | ||
<pre> | <pre> | ||
.mch for abstract machine files | |||
.ref for refinement machines | |||
.imp for implementation machines | |||
.def for DEFINITIONS files | |||
.rmch for Rules machines for data validation | |||
</pre> | </pre> | ||
=== Differences with AtelierB/B4Free=== | === Free Types === | ||
More information can be found [[Free Types|here]]. | |||
Free types exist in Z and in the Rodin theory plugin and are supported by ProB. | |||
You can also define new free types in classical B by adding a ''FREETYPES'' clause with free type definitions separated by semicolon. | |||
Here is a definition of an inductive type ''IntList'' for lists of integers constructed using ''inil'' and ''icons'': | |||
<pre> | |||
FREETYPES | |||
IntList = inil, icons(INTEGER*IntList) | |||
</pre> | |||
=== Differences with AtelierB/B4Free === | |||
Basically, ProB tries to be compatible with Atelier B and conforms to the semantics | Basically, ProB tries to be compatible with Atelier B and conforms to the semantics | ||
of Abrial's B-Book and of [http://www.atelierb.eu/php/documents-en.php#manuel-reference Atelier B's reference manual]. | of Abrial's B-Book and of [http://www.atelierb.eu/php/documents-en.php#manuel-reference Atelier B's reference manual]. | ||
Here are the main differences with Atelier B: | Here are the main differences with Atelier B: | ||
<pre> | <pre> | ||
- tuples without parentheses are not supported; write (a,b,c) instead of a,b,c | |||
- relational composition has to be wrapped into parentheses; write (f;g) | |||
- parallel product also has to be wrapped into parentheses; write (f||g) | |||
- not all tree operators are supported | |||
- the VALUES clause is only partially supported | |||
- definitions have to be syntactically correct and be either an expression, | |||
predicate or substitution; | |||
the arguments to definitions have to be expressions; | |||
definitions which are predicates or substitutions must be declared before first use | |||
- definitions are local to a machine | |||
- for ProB the order of fields in a record is not relevant (internally the fields are | |||
sorted), Atelier-B reports a type error if the order of the name of the fields changes | |||
- well-definedness: for disjunctions and implications ProB uses the L-system | |||
of well-definedness (i.e., for P => Q, P should be well-defined and | |||
if P is true then Q should also be well-defined) | |||
- ProB allows WHILE loops and sequential composition in abstract machines | |||
- ProB now allows the IF-THEN-ELSE and LET for expressions and predicates | |||
(e.g., IF x<0 THEN -x ELSE x END or LET x BE x=f(y) IN x+x END) | |||
- ProB's type inference is stronger than Atelier-B's, much less typing predicates | |||
are required | |||
- You can apply prj1 and prj2 without providing the type arguments, e.g., prj2(prj1(1|->2|->3)) | |||
- ProB accepts operations with parameters but without pre-conditions | |||
- ProB allows identifiers consisting of a single character and identifiers in single backquotes (`id`) | |||
- ProB allows to use <> for the empty sequence (but this use is deprecated) | |||
- ProB allows escape codes (\n, \', \", see above) and supports UTF-8 characters in strings, | |||
( | and ProB allows multi-line string literals written using three apostrophes ('''string''') | ||
as well as template strings using three backquotes (e.g., ```1+2=${1+2}```) | |||
- ProB allows a she-bang line in machine files starting with #! | |||
- ProB allows btrue and bfalse as predicates in B machines | |||
- ProB allows to use the Event-B relation operators <<->, <->>, <<->> | |||
- ProB allows set comprehensions with an extra expression like {x•x:1..10|x*x}. | |||
- The FREETYPES section and the external libraries (LibraryStrings.def, ...) do not exist in Atelier-B | |||
</pre> | </pre> | ||
Line 493: | Line 556: | ||
<pre> | <pre> | ||
- AtelierB/ProB do not allow true as predicate; | - AtelierB/ProB do not allow true as predicate; | ||
e.g., PRE true THEN ... END is not allowed (use BEGIN ... END instead) | e.g., PRE true THEN ... END is not allowed (use BEGIN ... END instead) | ||
ProB now allows btrue and bfalse to be used as predicates. | |||
- AtelierB/ProB do not allow a machine parameter to be used in the PROPERTIES | - AtelierB/ProB do not allow a machine parameter to be used in the PROPERTIES | ||
- AtelierB/ProB require a scalar machine parameter to be typed in the | - AtelierB/ProB require a scalar machine parameter to be typed in the | ||
Line 500: | Line 564: | ||
</pre> | </pre> | ||
=== Other notes=== | If you discover more differences, please let us know! | ||
=== Other notes === | |||
<pre> | <pre> | ||
ProB now supports the Unicode mathematical symbols, exactly like Atelier-B | |||
ProB is best at treating universally quantified formulas of the form | ProB is best at treating universally quantified formulas of the form | ||
!x.(x:SET => RHS), or | |||
!(x,y).(x|->y:SET =>RHS), | |||
!(x,y,z).(x|->y|->z:SET =>RHS), ...; | |||
otherwise the treatment of !(x1,...,xn).(LHS => RHS) may delay until all values | otherwise the treatment of !(x1,...,xn).(LHS => RHS) may delay until all values | ||
treated by LHS are known. | treated by LHS are known. | ||
Line 511: | Line 579: | ||
The construction S:FIN(S) is recognised by ProB as equivalent to the Event-B | The construction S:FIN(S) is recognised by ProB as equivalent to the Event-B | ||
finite(S) operator. | finite(S) operator. | ||
ProB assumes that machines and STRING values are encoded using UTF-8. | ProB assumes that machines and STRING values are encoded using UTF-8. | ||
</pre> | </pre> | ||
=== Event-B Syntax === | |||
Note that the Event-B syntax in Rodin is slightly different (e.g, no sequences or strings built-in). There is also an Event-B summary by Ken Robinson ([[File:EventB-summary.pdf|PDF File]]). The Event-B syntax is only available for Event-B models in Rodin, ProB2-UI and ProB Jupyter notebooks. | |||
{{Feedback}} | {{Feedback}} |
Below we describe the "classical" B syntax as supported by ProB. You may also wish to consult
P & Q conjunction P or Q disjunction P => Q implication P <=> Q equivalence not(P) negation !(x).(P=>Q) universal quantification #(x).(P&Q) existential quantification btrue truth (this is a predicate) bfalse falsity (this is a predicate)
Above, P and Q stand for predicates. Inside the universal quantification, P must give a value type to the quantified variable. Note: you can also introduce multiple variables inside a universal or existential quantification, e.g., !(x,y).(P => Q).
E = F equality E /= F disequality
TRUE truth value (this is an expression) FALSE falsity value (this is an expression) BOOL set of boolean values ({TRUE,FALSE}) bool(P) convert predicate into BOOL value
Warning: TRUE and FALSE are expression values and not predicates in B and cannot be combined using logical connectives. To combine two boolean values x and y using conjunction you have to write x=TRUE & y=TRUE. To convert a predicate such as z>0 into a boolean value you have to use bool(z>0).
{} empty set {E} singleton set {E,F} set enumeration {x|P} comprehension set {(x).P|E} Event-B style comprehension set (brackets needed) POW(S) power set POW1(S) set of non-empty subsets FIN(S) set of all finite subsets FIN1(S) set of all non-empty finite subsets card(S) cardinality S*T cartesian product S\/T set union S/\T set intersection S-T or S \ T set difference E:S element of E/:S not element of S<:T subset of S/<:T not subset of S<<:T strict subset of S/<<:T not strict subset of union(S) generalised union over sets of sets inter(S) generalised intersection over sets of sets UNION(z).(P|E) generalised union with predicate INTER(z).(P|E) generalised intersection with predicate
INTEGER set of integers NATURAL set of natural numbers NATURAL1 set of non-zero natural numbers INT set of implementable integers (MININT..MAXINT) NAT set of implementable natural numbers NAT1 set of non-zero implementable natural numbers n..m set of numbers from n to m MININT the minimum implementable integer MAXINT the maximum implementable integer m>n greater than m<n less than m>=n greater than or equal m<=n less than or equal max(S) maximum of a set of numbers min(S) minimum of a set of numbers m+n addition m-n difference m*n multiplication m/n division m**n power m mod n remainder of division PI(z).(P|E) set product SIGMA(z).(P|E) set summation succ(n) successor (n+1) pred(n) predecessor (n-1) 0xH hexadecimal literal, where H is a sequence of letters in [0-9A-Fa-f]
S<->T relation S<<->T total relation S<->>T surjective relation S<<->>T total surjective relation E|->F maplet dom(r) domain of relation ran(r) range of relation id(S) identity relation S<|r domain restriction S<<|r domain subtraction r|>S range restriction r|>>S range subtraction r~ inverse of relation r[S] relational image r1<+r2 relational overriding (r2 overrides r1) r1><r2 direct product (all pairs (x,(y,z)) with x,y:r1 and x,z:r2) (r1;r2) relational composition {x,y| x|->z:r1 & z|->y:r2} (r1||r2) parallel product (all pairs ((x,v),(y,w)) with x,y:r1 and v,w:r2) prj1(S,T) projection function (usage prj1(Dom,Ran)(Pair)) prj2(S,T) projection function (usage prj2(Dom,Ran)(Pair)) prj1(Pair) and prj2(Pair) are also allowed fnc(r) translate relation A<->B into function A+->POW(B) rel(r) translate relation A<->POW(B) into relation A<->B closure1(r) transitive closure closure(r) reflexive & transitive closure (equal to id(TYPEOF_r) \/ closure1(r)) iterate(r,n) iteration of r with n>=0 (Note: iterate(r,0)=id(s) where s=TYPEOF_r)
S+->T partial function S-->T total function S+->>T partial surjection S-->>T total surjection S>+>T partial injection S>->T total injection S>+>>T partial bijection S>->>T total bijection %x.(P|E) lambda abstraction f(E) function application f(E1,...,En) is also supported (as well as f(E1|->E2...|->En))
[] or <> empty sequence [E] singleton sequence [E,F] constructed sequence seq(S) set of sequences over S seq1(S) set of non-empty sequences over S iseq(S) set of injective sequences over S iseq1(S) set of non-empty injective sequences over S perm(S) set of bijective sequences (permutations) over S size(s) size of sequence s^t concatenation E->s prepend element s<-E append element rev(s) reverse of sequence first(s) first element last(s) last element front(s) front of sequence (all but last element) tail(s) tail of sequence (all but first element) conc(S) concatenation of sequence of sequences s/|\n take first n elements of sequence s\|/n drop first n elements from sequence
struct(ID:S,...,ID:S) set of records with given fields and field types rec(ID:E,...,ID:E) construct a record with given field names and values E'ID get value of field with name ID
ID must start with letter (ASCII or Unicode), can then contain letters (ASCII or Unicode), digits and underscore (_) and can end with Unicode subscripts followed by Unicode primes M.ID composed identifier for identifier coming from included machine M `ID` an identifier in backquotes can contain almost any character (except newline)
"astring" a specific (single-line) string value '''astring''' an alternate way of writing (multi-line) strings, no need to escape " ```tstring``` template strings, where ${Expr} parts are evaluated and converted to string, you can provide options separated by commas in square brackets like $[2f]{Expr}. Valid options are: Nf (for floats/reals), Nd (for integer), Np (padding), ascii (can be abbreviated to a), unicode (can be abbreviated to u). STRING the set of all strings
Atelier-B does not support any operations on strings, apart from equality and disequality. In ProB, however, some of the sequence operators work also on strings:
size(s) the length of a string s rev(s) the reverse of a string s s ^ t the concatenation of two strings conc(ss) the concatenation of a sequence of strings
You can turn this support off using the STRING_AS_SEQUENCE preference. The library LibraryStrings.def in stdlib contains additional useful external functions (like TO_STRING, STRING_SPLIT, FORMAT_TO_STRING, INT_TO_HEX_STRING, ...).
ProB also allows multi-line strings.
As of version 1.7.0, ProB will support the following escape sequences within strings:
\n newline (ASCII character 13) \r carriage return (ASCII 10) \t tab (ASCII 9) \" the double quote symbol " \' the single quote symbol ' \\ the backslash symbol
Within single-line string literals, you do not need to escape '. Within multi-line string literals, you do not need to escape " and you can use tabs and newlines.
ProB assumes that all B machines and strings use the UTF-8 encoding.
REAL set of reals FLOAT set of floating point numbers i.f real literal in decimal notation, where i and f are natural numbers i.fEg real literal in scientific notation, where i,f are natural numbers and g is an integer real(n) convert an integer n into a real number floor(r) convert a real r into an integer ceiling(r) convert a real r into an integer
One can also use a lowercase e for literals in scientific notation (e.g. 1.0e-10). Standard arithmetic operators can be applied to reals: +, - , *, /, SIGMA, PI. Exponentiation of a real with an integer is also allowed. The comparison predicates =, /=, <, >, <=, >= also all work. Support for reals and floats is experimental. The definition in Atelier-B is also not stable yet. Currently ProB supports floating point numbers only. Warning: properties such as associativity and commutativity of arithmetic operators thus do not hold. The library LibraryReals.def in stdlib contains additional useful external functions (like RSIN, RCOS, RLOG, RSQRT, RPOW, ...). You can turn off support for REALS using the preference ALLOW_REALS. The REAL_SOLVER preference how constraints are solved.
Nodes in the tree are denoted by index sequences (branches), e.g, n=[1,2,1] Each node in the tree is labelled with an element from a domain S. A tree is a function mapping of branches to elements of the domain S.
tree(S) set of trees over domain S btree(S) set of binary trees over domain S top(t) top of a tree const(E,s) construct a tree from info E and sequence of subtrees s rank(t,n) rank of the node at end of branch n in the tree t father(t,n) father of the node denoted by branch n in the tree t son(t,n,i) the ith son of the node denoted by branch n in tree t sons(t) the sequence of sons of the root of the tree t subtree(t,n) arity(t,n) bin(E) construct a binary tree with a single node E bin(tl,E,tr) construct a binary tree with root info E and subtrees tl,tr left(t) the left (first) son of the root of the binary tree t right(t) the right (last) son of the root of the binary tree t sizet(t) the size of the tree (number of nodes) prefix(t) the nodes of the tree t in prefix order postfix(t) the nodes of the tree t in prefix order mirror, infix are recognised by the parser but not yet supported by ProB itself
ProB allows the following for predicates, expressions and substitutions:
IF P THEN E1 END conditional branching IF P THEN E1 ELSIF E2 END we also allow multiple ELSIF branches IF P THEN E1 ELSE E2 END but you always need an ELSE branch for expressions and predicates IF P THEN E1 ELSIF E2 ELSE E3 END LET x1,... BE x1=E1 & ... IN E END introduce local variables
Note: the expression Ei defining xi is allowed to use x1,...,x(i-1) for predicates/expressions. By setting the preference ALLOW_COMPLEX_LETS to TRUE, this is also allowed for substitutions.
skip no operation x := E assignment f(x) := E functional override x :: S choice from set x : (P) choice by predicate P (constraining x; previous value of x is x$0) x <-- OP(x) call operation and assign return value G||H parallel substitution** G;H sequential composition** ANY x,... WHERE P THEN G END non deterministic choice LET x,... BE x=E & ... IN G END VAR x,... IN G END generate local variables PRE P THEN G END ASSERT P THEN G END CHOICE G OR H END IF P THEN G END IF P THEN G ELSE H END IF P1 THEN G1 ELSIF P2 THEN G2 ... END IF P1 THEN G1 ELSIF P2 THEN G2 ... ELSE Gn END SELECT P THEN G WHEN ... WHEN Q THEN H END SELECT P THEN G WHEN ... WHEN Q THEN H ELSE I END CASE E OF EITHER m THEN G OR n THEN H ... END END CASE E OF EITHER m THEN G OR n THEN H ... ELSE I END END WHILE P1 DO G INVARIANT P2 VARIANT E END WHEN P THEN G END is a synonym for SELECT P THEN G END
**: cannot be used at the top-level of an operation, but needs to be wrapped inside a BEGIN END or another statement (to avoid confusion with the operators ; and || on relations).
MACHINE or REFINEMENT or IMPLEMENTATION
Note: machine parameters can either be SETS (if identifier is all upper-case) or scalars (i.e., integer, boolean or SET element; if identifier is not all upper-case; typing must be provided be CONSTRAINTS)
You can also use MODEL or SYSTEM as a synonym for MACHINE, as well as EVENTS as a synonym for OPERATIONS. ProB also supports the ref keyword of Atelier-B for event refinement.
CONSTRAINTS P (logical predicate) SETS S;T={e1,e2,...};... FREETYPES x=x1,x2(arg2),...;... CONSTANTS x,y,... CONCRETE_CONSTANTS cx,cy,... PROPERTIES P (logical predicate) DEFINITIONS m(x,...) == BODY;... VARIABLES x,y,... CONCRETE_VARIABLES cv,cw,... INVARIANT P (logical predicate) ASSERTIONS P;...;P (list of logical predicates separated by ;) INITIALISATION S (substitution) OPERATIONS O;... (operations)
USES list of machines INCLUDES list of machines SEES list of machines EXTENDS list of machines PROMOTES list of operations REFINES machine
Note: Refinement machines should express the operation preconditions in terms of their own variables.
NAME1 == Expression; Definition without arguments NAME2(ID,...,ID) == E2; Definition with arguments "FILE.def"; Include definitions from file
There are a few specific definitions which can be used to influence ProB:
GOAL == P to define a custom Goal predicate for Model Checking (the Goal is also set by using "Advanced Find...") SCOPE == P to limit the search space to "interesting" nodes scope_SETNAME == n..n to define custom cardinality for set SETNAME scope_SETNAME == n equivalent to 1..n SET_PREF_MININT == n SET_PREF_MAXINT == n SET_PREF_MAX_INITIALISATIONS == n max. number of intialisations computed SET_PREF_MAX_OPERATIONS == n max. number of enablings per operation computed MAX_OPERATIONS_OPNAME == n max. number of enablings for the operation OPNAME SET_PREF_SYMBOLIC == TRUE/FALSE SET_PREF_TIME_OUT == n time out for operation computation in ms ASSERT_LTL... == "LTL Formula" using X,F,G,U,R LTL operators + Y,O,H,S Past-LTL operators + atomic propositions: e(OpName), [OpName], {BPredicate} HEURISTIC_FUNCTION == n in directed model-checking mode nodes with smalles value will be processed first
The following definitions allow providing a custom state visualization (n can be empty or a number):
ANIMATION_FUNCTIONn == e a function (INT*INT) +-> INT or an INT ANIMATION_FUNCTION_DEFAULT == e a function (INT*INT) +-> INT or an INT instead of any INT above you can also use BOOL or any SET as a result you can also use STRING values, or even other values which are pretty printed ANIMATION_IMGn == "PATH to .gif" a path to a gif file ANIMATION_STRn == "sometext" a string without spaces; the result integer n will be rendered as a string ANIMATION_STR_JUSTIFY_LEFT == TRUE computes the longest string in the outputs and pads the other strings accordingly SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == n additional padding between images in pixels SET_PREF_TK_CUSTOM_STATE_VIEW_STRING_PADDING == n additional padding between text in pixels
The following definitions allow providing a custom state graph (n can be empty or a number):
CUSTOM_GRAPH_NODESn == e define a set of nodes to be shown, nodes can also be pairs (Node,Colour), triples (Node,Shape,Colour) or records or sets of records like rec(color:Colour, shape:Shape, style:Style, label:Label, value:Node, ...) Colours are strings of valid Dot/Tk colors (e.g., "maroon" or "red") Shapes are strings of valid Dot shapes (e.g., "rect" or "hexagon"), and Styles are valid Dot shape styles (e.g., "rounded" or "solid" or "dashed") CUSTOM_GRAPH_EDGESn == e define a relation to be shown as a graph edges can either be pairs (node1,node2) or triples (node1,Label,node2) where Label is either a Dot/Tk color or a string or value representing the label to be used for the edges
In both cases e can also be a record which defines default dot attributes like color, shape, style and description, e.g.:
CUSTOM_GRAPH_NODES == rec(color:"blue", shape:"rect", style:"filled", nodes:e); CUSTOM_GRAPH_EDGES == rec(color:"red", style:"dotted", dir:"none", penwidth:2, edges:e)
Alternatively, the complete graph can be put into one definition using CUSTOM_GRAPH
.
You have to define a single CUSTOM_GRAPH definition of a record with global graph attributes
(like rankdir or layout) and optionally with edges and nodes attributes (replacing CUSTOM_GRAPH_EDGES and CUSTOM_GRAPH_NODES respectively), e.g.:
CUSTOM_GRAPH == rec(layout:"circo", nodes:mynodes, edges:myedges)
You can now also use a single CUSTOM_GRAPH definition of a record with global graph attributes (like rankdir or layout) and optionally with edges and nodes attributes (replacing CUSTOM_GRAPH_EDGES and CUSTOM_GRAPH_NODES respectively), e.g.:
CUSTOM_GRAPH == rec(layout:"circo", nodes:mynodes, edges:myedges)
You can also provide SEQUENCE_CHART_opname definitions for generating UML sequence charts.
These DEFINITIONS affect VisB:
VISB_JSON_FILE == "PATH to .json" a path to a default VisB JSON file for visualisation; if it is "" an empty SVG will be created VISB_SVG_OBJECTSn == ... define a record or set of records for creating new SVG objects VISB_SVG_UPDATESn == ... define a record or set of records containing updates of SVG objects VISB_SVG_HOVERSn == ... define a record or set of records for VisB hover functions VISB_SVG_BOX == ... record with dimensions (height, width) of a default empty SVG VISB_SVG_CONTENTS == ... defines a string to be included into a created empty SVG file
B supports two styles of comments: /* ... */ block comments // ... line comments
ProB recognises several pragma comments of the form /*@ PRAGMA VALUE */ The whitespace between @ and PRAGMA is optional.
/*@symbolic */ put before comprehension set, lambda, union or composition to instruct ProB to keep it symbolic and not try to compute it explicitly /*@label LBL */ associates a label LBL with the following predicate (LBL must be identifier or a string "....") /*@desc DESC */ associates a description DESC with the preceding predicate or introduced identifier (in VARIABLES, CONSTANTS,... section) There are three special descriptions: /*@desc memo*/ to be put after identifiers in the ABSTRACT_CONSTANTS section indicating that these functions should be memoized /*@desc expand*/ to be put after identifiers (in VARIABLES, CONSTANTS,... section) indicating that they should be expanded and not kept symbolically /*@desc prob-ignore */ to be put after predicates (e.g., in PROPERTIES) which should be ignored by ProB when the preference USE_IGNORE_PRAGMAS is TRUE /*@file PATH */ associates a file for machines in SEES, INCLUDES, ... put pragma after a seen or included machine /*@package NAME */ at start of machine, machine file should be in folder NAME/... NAME can be qualified N1.N2...Nk, in which case the machine file should be in N1/N2/.../Nk /*@import-package NAME */ adds ../NAME to search paths for SEES,... NAME can also be qualified N1.N2...Nk, use after package pragma /*@generated */ can be put at the top of a machine file; indicates the machine is generated from some other source
.mch for abstract machine files .ref for refinement machines .imp for implementation machines .def for DEFINITIONS files .rmch for Rules machines for data validation
More information can be found here.
Free types exist in Z and in the Rodin theory plugin and are supported by ProB. You can also define new free types in classical B by adding a FREETYPES clause with free type definitions separated by semicolon.
Here is a definition of an inductive type IntList for lists of integers constructed using inil and icons:
FREETYPES IntList = inil, icons(INTEGER*IntList)
Basically, ProB tries to be compatible with Atelier B and conforms to the semantics of Abrial's B-Book and of Atelier B's reference manual. Here are the main differences with Atelier B:
- tuples without parentheses are not supported; write (a,b,c) instead of a,b,c - relational composition has to be wrapped into parentheses; write (f;g) - parallel product also has to be wrapped into parentheses; write (f||g) - not all tree operators are supported - the VALUES clause is only partially supported - definitions have to be syntactically correct and be either an expression, predicate or substitution; the arguments to definitions have to be expressions; definitions which are predicates or substitutions must be declared before first use - definitions are local to a machine - for ProB the order of fields in a record is not relevant (internally the fields are sorted), Atelier-B reports a type error if the order of the name of the fields changes - well-definedness: for disjunctions and implications ProB uses the L-system of well-definedness (i.e., for P => Q, P should be well-defined and if P is true then Q should also be well-defined) - ProB allows WHILE loops and sequential composition in abstract machines - ProB now allows the IF-THEN-ELSE and LET for expressions and predicates (e.g., IF x<0 THEN -x ELSE x END or LET x BE x=f(y) IN x+x END) - ProB's type inference is stronger than Atelier-B's, much less typing predicates are required - You can apply prj1 and prj2 without providing the type arguments, e.g., prj2(prj1(1|->2|->3)) - ProB accepts operations with parameters but without pre-conditions - ProB allows identifiers consisting of a single character and identifiers in single backquotes (`id`) - ProB allows to use <> for the empty sequence (but this use is deprecated) - ProB allows escape codes (\n, \', \", see above) and supports UTF-8 characters in strings, and ProB allows multi-line string literals written using three apostrophes ('''string''') as well as template strings using three backquotes (e.g., ```1+2=${1+2}```) - ProB allows a she-bang line in machine files starting with #! - ProB allows btrue and bfalse as predicates in B machines - ProB allows to use the Event-B relation operators <<->, <->>, <<->> - ProB allows set comprehensions with an extra expression like {x•x:1..10|x*x}. - The FREETYPES section and the external libraries (LibraryStrings.def, ...) do not exist in Atelier-B
See also our Wiki for documentation:
Also note that there are various differences between BToolkit and AtelierB/ProB:
- AtelierB/ProB do not allow true as predicate; e.g., PRE true THEN ... END is not allowed (use BEGIN ... END instead) ProB now allows btrue and bfalse to be used as predicates. - AtelierB/ProB do not allow a machine parameter to be used in the PROPERTIES - AtelierB/ProB require a scalar machine parameter to be typed in the CONSTRAINTS clause - In AtelierB/ProB the BOOL type is pre-defined and cannot be redefined
If you discover more differences, please let us know!
ProB now supports the Unicode mathematical symbols, exactly like Atelier-B ProB is best at treating universally quantified formulas of the form !x.(x:SET => RHS), or !(x,y).(x|->y:SET =>RHS), !(x,y,z).(x|->y|->z:SET =>RHS), ...; otherwise the treatment of !(x1,...,xn).(LHS => RHS) may delay until all values treated by LHS are known. Similarly, expressions of the form SIGMA(x).(x:SET|Expr) and PI(x).(x:SET|Expr) lead to better constraint propagation. The construction S:FIN(S) is recognised by ProB as equivalent to the Event-B finite(S) operator. ProB assumes that machines and STRING values are encoded using UTF-8.
Note that the Event-B syntax in Rodin is slightly different (e.g, no sequences or strings built-in). There is also an Event-B summary by Ken Robinson (File:EventB-summary.pdf). The Event-B syntax is only available for Event-B models in Rodin, ProB2-UI and ProB Jupyter notebooks.
Please help us to improve this documentation by providing feedback in our bug tracker, asking questions in our prob-users group or sending an email to Michael Leuschel.