formal-verification - B规范的细化

Question

考虑我在 B 规范中有以下内容：-

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

我是否可以创建如下改进：-

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

Answer 1

不，这是不可能的，因为在细化中，变量的类型必须与规范中的类型相同（如果规范中存在同名的变量，就像这里一样）。