Non-determinism

Commands used for non-determinism on B-method

It is an important feature using abstract specifications because it allows some decisions to be made later at appropriate time in development

Commands used for non-determinism on B-method

So far, we've learnt how to code deterministic operations. These depended only on the initialization and the input values

Non-deterministic assignment

CHOICE

ANY

PRE

SELECT

LET

Non-deterministic commands

Non-deterministic assignment

PRE

ANY

ANY x WHERE Q THEN T END

Q is a predicate, which types x

T is a machine command, in other words, the body of the command

x is a new variable, whose scope is within the common "ANY"

It is possible to have more than one variable

You can use the command ANY to assign a random element from a set to a variable

There is a shortcut to this operation: xx :: S This means a random value of S will be assigned to xx

It is also possible to assign random subsets to a variable

team :: {tt | tt <: squad and card(tt) = 11}

team is a random subset of squad, which has 11 elements

CHOICE

It can choose any of the commands given to execute

SELECT

It allows to choose an option depending on whether it is enabled or not

Each option has a condition called guard that enables the option if the condition is true

LET

This operation is an example of non-determinism because we can't know for sure which values will be chosen. These values have to respect the preconditions

LET xx be xx = E in S END

xx is a new variable, whose scope is within the common "LET"

The value of xx is defined by the expression E

S is executed with xx in scope