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}

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.

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

encodes

if PRED then C1 else C2

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].