B Machines: Introduction and Operations
Uploaded by
gperson98B Machines: Introduction and Operations
Uploaded by
gperson98Introducing B Machines
Michael Butler, University of Southampton
1
MACHINE Counter OPERATIONS
Inc =
ˆ PRE
CONSTANTS max
ctr < max
PROPERTIES max ∈ N THEN
ctr := ctr + 1
VARIABLES ctr END
INVARIANT
Dec =
ˆ PRE
ctr ∈ N ∧
ctr > 0
THEN
0 ≤ ctr ≤ max
ctr := ctr − 1
END
INITIALISATION ctr := 0 val ←− Display =
ˆ
val := ctr
2
MACHINE Dictionary OPERATIONS
AddW ord(w) =ˆ
SETS W ord
PRE
w ∈ W ord
VARIABLES known THEN
INVARIANT known := known ∪ {w}
END
known ⊆ W ord
res ←− CheckW ord(w) = ˆ
PRE
w ∈ W ord
INITIALISATION dict := {} THEN
res := bool(w ∈ known)
END
3
B machine contains
• Sets: abstract types used in specification
• Constants: logical variables who’s value remain constant
• Properties: constraints on the constants. A property is a
logical predicate.
• Variables: state variables who’s values can change
• Invariants: constraints on the variables that should always
hold true. An invariant is a logical predicate.
• Initialisation: initial values for the abstract variables
• Operations: operations specifying ways in which the abstract
variables can change
4
Operation Preconditions
Inc =
ˆ PRE
ctr < max Precondition
THEN
ctr := ctr + 1 Body
END
A precondition is a predicate on the variables. An operation
should only be called when its precondition is true.
The body of an operation assigns new values to the state vari-
ables. The body of an operation should maintain the invariant
provided the precondition holds before the operation is executed.
Why does Inc preserve the invariant ctr ≤ max ?
5
Operation Parameters
Operations can have input parameters and output parameters:
res ←− CheckW ord(w) = ˆ
PRE
w ∈ W ord
THEN
res := bool(w ∈ dict)
END
w is an input parameter. Its type is determined by the precon-
dition.
res is an output parameter. Its return value is determined by an
assignment to res. Its type is inferred from the type of the value
assigned to it.
6
Multiple Assignment
An operation body (and a machine initialisation) can have mul-
tiple assignments separated by ||.
MACHINE CountingDictionary OPERATIONS
SETS W ord
AddW ord(w) = ˆ
PRE
VARIABLES known, count w ∈ W ord
INVARIANT THEN
known := known ∪ {w} ||
known ⊆ W ord ∧ count := count + 1
count ∈ N ∧ END
count = card(known)
7
Multiple Assignment
An operation body (and a machine initialisation) can have mul-
tiple assignments separated by ||.
MACHINE CountingDictionary OPERATIONS
SETS W ord
AddW ord(w) = ˆ
PRE
VARIABLES known, count w ∈ W ord
INVARIANT THEN
known := known ∪ {w} ||
known ⊆ W ord ∧ count := count + 1
count ∈ N ∧ END
count = card(known)
Can anyone spot an error with this specification?
8