La syntaxe B ASCII

Toutes les formes syntaxiques de B ne sont pas ci-dessous. Sont présentes celles prises en compte par proB.

Logical predicates:
-------------------
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

Equality:
---------
E = F equality
E /= F disequality

Sets:
-----
{} empty set
{E} singleton set
{E,F} set enumeration
{x|P} comprehension set
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 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 Numbers: -------- 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 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 Relations: ---------- S<->T 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 right overriding r1+>r2 left overriding
r1>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 now supported (as well as f(E1|->E2))

Sequences:
----------
<> empty sequence
[E] singleton sequence
[E,F] constructed sequence
seq(S) set of sequences over Sequence
seq1(S) set of non-empty sequences over S
iseq(S) set of injective sequences
iseq1(S) set of non-empty injective sequences
perm(S) set of bijective sequences (permutations)
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
s\|/n drop

Records:
--------
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

Trees:
------
left, right, tree, btree, ... are recognised by the parser but not yet
supported by ProB itself
Statements:
-----------
skip no operation
x:= E assignment
f(x) := E functional override
x::S choice from set
x : P choice by predicate P (constraining x)
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
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
CASE E OF EITHER m THEN G OR n THEN H ... ELSE I END

Machine header:
---------------
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)

Machine sections:
-----------------
SETS
CONSTANTS
PROPERTIES
DEFINITIONS
VARIABLES
INVARIANT
INITIALISATION
OPERATIONS

Machine inclusion:
------------------
USES list of machines
INCLUDES list of machines
SEES list of machines
EXTENDS list of machines
PROMOTES list of operations
REFINES machine



Definitions:
------------
NAME1 == Expression ; NAME2(ID,...,ID) == E2 ...