Refinement of a B specification

85 views Asked by At

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
1

There are 1 answers

0
danielp On BEST ANSWER

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