B中联合和量化联合的区别？答案

【问题标题】：Difference between union and quantified union in B?B中联合和量化联合的区别？
【发布时间】：2017-11-12 20:37:29
【问题描述】：

我目前正在使用 Atelier B，希望更好地了解 union 和 quantified union 之间的区别。一个例子将不胜感激

【问题讨论】：

【解决方案1】：

联合是一个二元运算符：它有两个参数，两个集合并返回这两个集合的联合。例如：

{1, 2} \/ {2, 4}

是

{1, 2, 4}

此运算符具有关联性和可交换性，因此您可以组合此运算符的多个应用而无需使用括号。例如：

{ 1, 2 } \/ {2, 3, 4, 5} \/ {1, 3, 5, 7}

是

{ 1, 2, 3, 4, 5, 7}

第二个运算符是量化联合。它是一个三元运算符，具有三个参数：标识符列表，例如 x1...xn，谓词，例如 P(x1...xn) 和表达式，例如 E(x1...xn)。表达式 E(x1...xn) 必须是一个集合。结果是所有集合 E(x1...xn) 的并集，使得 P(x1...xn) 成立。比如

UNION(x1, x2) . (x1 : {1, 2, 3} & x2 : {10, 20} | { x1 + x2 })

是

{ 1+10 } \/ { 1+20 } \/ { 2+10 } \/ { 2+20 } \/ { 3+10 } \/ { 3+20 }

简化为：

{ 11, 12, 13, 21, 22, 23 }.

量化联合的第二个例子：

UNION(low, upp).(low : {10, 20} & upp: {12, 14} | { xx | xx : INT & low <= xx & xx <= upp })

是

{ xx | xx : INT & 10 <= xx & xx <= 12 } \/ 
{ xx | xx : INT & 10 <= xx & xx <= 14 } \/ 
{ xx | xx : INT & 20 <= xx & xx <= 12 } \/ 
{ xx | xx : INT & low <= 20 & xx <= 14 }

简化为

{ 10, 11, 12 } \/ { 10, 11, 12, 13, 14 } \/ {} \/ {}

这反过来又简化为

{ 10, 11, 12, 13, 14 }

【讨论】：