我不确定这是否适合 stackoverflow,但我不知道还有什么地方可以问。我正在研究用于证明需求规范一致性的 B 方法,但在指定操作的前提条件时我对逻辑数学符号有疑问。
简化原始问题,我有一个变量,它是 FLIGHT_NO x TIME x TIME 之间的笛卡尔积的子集 flights,其中对于每个成员 (no,td,ta),不意味着航类号,td 起飞时间和 ta 到达时间。如何使用数学逻辑符号获取 flights 中具有最大 td 值的元素?
最佳答案
您想获取这样的元素,还是要测试您拥有的元素是否满足此属性?我问是因为第二个似乎是手术的明智先决条件。我不是特别了解 B-Method;我看过一些文档,但找不到快速引用,所以这在某些细节上可能是错误的。
第二个应该如下所示(prj2
用于第二个投影):
HasGreatestTd(flight) = flight \in flights \and \forall flight' (flight' \in flights => prj2(flight) >= prj2(flight'))
那么第一个是:
flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})
关于math - AMN 和数学逻辑符号,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/1893482/