Tips: B Idioms: Difference between revisions

Also have a look at Tips:_Writing_Models_for_ProB.

Let

Classical B only has a LET substitution, no let construct for predicates or expressions. Event-B has no let construct whatsoever.

Let for predicates

For predicates this encodes a let predicate:

#x.(x=E & P)

corresponds to something like

let x=E in P

Within set comprehensions one can use the following construct:

dom({x,y|y=E & P})

corresponds to something like

{x|let y=E in P}

One can also use the ran operator or introduce multiple lets in one go:

dom(dom({x,y,z|y=E1 & z=E2 &P}))

or

ran({y,z,x|y=E1 & z=E2 &P})

both encode

{x|let y=E1 & z=E2 in P}

Let for expressions

In case F is a set expression, then the following construct can be used to encode a let statement:

UNION(x).(x=E|F)

corresponds to something like

let x=E in F

The following construct has exactly the same effect:

INTER(x).(x=E|F)

If-Then-Else

Classical B only has an IF-THEN-ELSE substitution (aka statement), no such construct for predicates or expressions. The following construct

%((x).(x=0 & PRED|C1)\/%(x).(x=0 & not(PRED)|C2)) (0)

encodes an if-then-else for expressions:

if PRED then C1 else C2

It is recognised by ProB.

finite

In classical B there is no counterpart to the Event-B finite operator. However, the following construct has the same effect as finite(x) (and is recognised by ProB):

x : FIN(x)

all-different

One can encode the fact that n objects x1,...,xn are pair-wise different using the following construct (recognised by ProB):

card({x1,...,xn})=n

map

Given a function f and a sequence s one can map the function over all elements of s using the relational composition operator ;:

(s ; f)

For example, ([1,2,3] ; succ) gives us the sequence [2,3,4].

Recursion using closure1

Even though B has no built-in support for recursion, one can use the transitive closure operator closure1 to compute certain recursive functions. For this we need to encode the recursion as a step function of the form:

%(in,acc).(P|(inr,accr))

where P is a predicate which in case we have not yet reached a base case for the input value in. The computation result has to be stored in an accumulator: acc is the accumulator before the recursion step, accr after. inr is the new input value for the recursive call. In case the base case is reached for in, the predicate P should be false and the value of the recursive call should be the value of the accumulator.

The value of the recursive function can thus be obtained by calling:

closure1(step)[{(in,ia)}](b)

where in is the input value, b is the base case and ia is the initial (empty) accumulator.

For example, to sort a set of integers into a ascending sequence, we would define the step function as follows:

step = %(s,o).(s/={} | (s\{min(s)},o<-min(s)))

A particular call would be:

closure1(step)[{({4,5,2},[])}]({})

resulting in the sequence [2,4,5].

Observe that, even though closure1(step) is an infinite relation, ProB can compute the relational image of closure1(step) for a particular set such as {({4,5,2},[])} (provided the recursion terminates).