math - AMN 和数学逻辑符号

Question

我不确定这是否适合 stackoverflow，但我不知道还有什么地方可以问。我正在研究用于证明需求规范一致性的 B 方法，但在指定操作的前提条件时我对逻辑数学符号有疑问。

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

Answer 1

您想获取这样的元素，还是要测试您拥有的元素是否满足此属性？我问是因为第二个似乎是手术的明智先决条件。我不是特别了解 B-Method；我看过一些文档，但找不到快速引用，所以这在某些细节上可能是错误的。

第二个应该如下所示(prj2 用于第二个投影):

HasGreatestTd(flight) = flight \in flights \and \forall flight' (flight' \in flights => prj2(flight) >= prj2(flight'))

那么第一个是:

flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})