Please enable JavaScript.
Coggle requires JavaScript to display documents.
The B-Method: L10 - Coggle Diagram
The B-Method: L10
L10: Non-determinism
ANY
ANY x WHERE Q THEN T END
x is a new variable
Q is a predicate
T is a machine command
Non-deterministic assignment
xx :: S
Assign xx a random element of S
CHOICE
CHOICE S1
OR S2
OR ...
OR Sn
END
S1 ... Sn are machines commands
SELECT
SELECT P1 THEN S1
WHEN P2 THEN S2
...
WHEN Pn THEN Sn
ELSE Sm
END
P1 .. Pn are predicates
S1 .. Sm are machine commands
Operation pre-conditions (PRE)
PRE x > 0 THEN q := y / x END
The operation will be executed correctly only if the pre-condition is satisfied
LET (Deterministic)
LET it BE it = E IN S END
it is a new variable
E is an expression
S is a machine command