Разница между объединением и количественным объединением в B?

Question

В настоящее время я использую Atelier B и хотел бы лучше понять разницу между объединением и количественным определением объединения. Пример будет высоко ценится

Answer 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 }