formal-verificationformal-methodsrefinement-typeb-method

Refinement of a B specification

Consider I have the following in B specification :-

flower <: FLOWER
age <: AGE
owner <: OWNER
Type <: flower * age
Buyer : owner <-> flower

Is it possible for me to create a refinement as followed :-

flower <: FLOWER
age <: AGE
owner <: OWNER
Type : Owner <-> flower * age
Buyer : owner <-> flower
Solution

  • No, it is not possible because in a refinement a variable's type must have the same type as in the specification (if there is a variable with the same name in the specification like here).