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