Expressing rules in B-Method

Question

I'm writing some specifications of a system in B-method. I have the following variables which are subsets of a general set:

1. First Notation: a :={x,y,z,v} b :={x,y,z}

I want to state a rule that whenever something exists in set "b", it also exists in set "a" which helps writing the above specifications as the following:

2. second Notation: a :={v} b :={x,y,z}

Explanation of second notation: I want the machine to infer that a :={x,y,z,v} from a :={v}, b :={x,y,z}, and the rule.

How can I express the rule so I avoid the first notation and instead write the second notation?

I tried the following but it didn't work

INITIALISATION 
    a :={v} & 
    b :={x,y,z}
ASSERTIONS
    !x.(x:b => x:a)

Answer 1

First of all, the predicate !x.(x:b => x:a) can be more easily expressed just by b<:a.

It's not clear to me what exactly you want to express: Should b always be a subset of a or just in the initialisation?

If always, the INVARIANT would be the correct location for that. ASSERTIONS are similar but should be an implication by the other invariants. But then you must explicitly ensure that in your initialisation.

Another point which is unclear to me is what you mean by "infer". Do you just not want to specify the details? An initialisation where you assign a set with one element more than b could look like the following (assuming that a and b contain elements of S):

INITIALISATION
  ANY v,s
  WHERE
      v:S
    & s<:S
  THEN
      a := s\/{v}
   || b := s
  END

(Disclaimer: I haven't actually tested it.)

If a should always be larger than b, you could add something like v/:s. Your description does not make it clear what exactly you want to achieve.

Another approach would use the "becomes such substitution" (but in my opinion it is less readable):

INITIALISATION
     a,b :( a:S & b:S &
            b={x,y,z} & 
            #x.( x:S & a=b\/{x} ))

Answer 2

First, and foremost, the B machine does not infer anything by itself. It provides a language where the user can express properties and a mechanism that generates proof obligations that must be successfully processed by the prover (automatically or with human assistance) to guarantee that the properties hold.

In your example, if you want to express that every element of set bb is always an element of set aa, then as observed by danielp, just write

bb <: aa

Next, if you want to write that aa apossesses an element that is not in bb, then you can express it as

aa /= bb & not(aa = {})

or as

#(elem).(elem : S & elem : bb & not(elem : aa))

If you rather want to express that the specific value vv is in aa but not in bb, then the following applies

vv : bb & not(vv : aa)

These expressions may be used at several locations of the B machine, depending whether you want to assert properties on parameters, constants or variables.

For instance, say you have a machine with two variables va and vb, where both are sets of elements of a given set s1, and that you want they are initialized in such a way that every element of vb is also an element of va, and that there exists an element of va that is not in vb. Observe first that this means that vb is a strict subset of va.

INITIALISATION
  ANY inia, inib WHERE
    inia <: s1 & inib <: s2 & inib <<: inia
  THEN
    va := inia || vb := inib
  END