Tips: B Idioms

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

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

corresponds to something like

let x=E in F