CODEWITHSUNDEEP
formal-verificationformal-methodsrefinement-typeb-method
user1797730
user1797730

Reputation: 45

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

Upvotes: 1

Views: 80

Answers (1)

danielp
danielp

Reputation: 1187

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

Upvotes: 0

Related Questions