问题标签 [b-method]

我不确定这是否适合stackoverflow，但我不知道还能问哪里。我正在研究 B 方法以证明需求规范的一致性，在指定操作的前提条件时，我遇到了逻辑数学符号的问题。

简化原始问题，我有一个变量，它是FLIGHT_NO x TIME x TIME 之间笛卡尔积的子集航班，其中对于每个成员 (no,td,ta)，no 表示航班号，td 表示起飞时间和到达的时间。如何使用数学逻辑符号获得 具有最大 td 值的航班元素？

I heard about B-Method which is invented in France. Is it an alternative to traditional programming languages like c++ and java or is it a completely different thing with different purposes?

我不确定这是否适合stackoverflow，但我不知道还能问哪里。对于用b 语言编写的程序（不是 B 语言，C 和 C++ 的前身），我想知道它是否写得好，是否可以进行编译或测试？

我正在用 B 方法编写系统的一些规范。我有以下变量，它们是一般集合的子集：

1. 第一个符号：a :={x,y,z,v} b :={x,y,z}

我想声明一个规则，只要集合“b”中存在某些东西，它也存在于集合“a”中，这有助于将上述规范编写如下：

2. 第二种表示法：a :={v} b :={x,y,z}

第二个符号的解释：我希望机器从 a :={v}、b :={x,y,z} 和规则中推断出 a :={x,y,z,v}。

我怎样才能表达规则，所以我避免第一个符号，而是写第二个符号？

我尝试了以下但没有奏效

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

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