AMN 和数学逻辑符号
-
19-09-2019 - |
题
我不确定这是否适合 stackoverflow,但我不知道还能去哪里问。我正在研究 B 方法来证明需求规范的一致性,并且在指定操作的先决条件时,我对逻辑数学符号有疑问。
简化原始问题,我有一个变量,它是一个子集 航班 FLIGHT_NO x TIME x TIME 之间的笛卡尔积,其中对于每个成员 (no,td,ta),no 表示航班号,td 表示出发时间,ta 表示到达时间。我怎样才能使用数学逻辑符号得到元素 航班 哪个td值最大?
解决方案
你想要_____吗 得到 这样的元素,或者 测试 您拥有的元素满足此属性吗?我这么问是因为第二个似乎是手术的合理先决条件。我不太了解B法的具体情况;我查看了一些文档,但找不到快速参考,因此这在某些细节上可能是错误的。
第二个应该看起来像这样(prj2
用于第二次投影):
HasGreatestTd(flight) = flight \in flights \and \forall flight' (flight' \in flights => prj2(flight) >= prj2(flight'))
那么第一个是:
flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})
其他提示
请原谅我的无知,我不熟悉的B-方法。但不能使用独特量词?它会是这个样子:
存在一个时间td,使得对于所有时间TD 'TD> TD'
和
对于所有TD,TD 'TD '',如果TD> TD '' 和TD'> TD '' 然后TD TD =='
此,当然,假定有在该组恰好一个要素是。我真的不能告诉我们,如果B-方法允许一阶逻辑的全部力量,但是我认为你能来接近这个。
可以在 B 中定义函数。函数具有常量值,将在 ABSTRACT_CONSTANTS 子句中列出,并在 PROPERTIES 子句中定义。我尝试解释如何使用此结构来解决您的问题。
以下是一小段摘录
- 介绍了给出航班信息的笛卡尔积的快捷方式;
DEFINITIONS FLIGHT_INFO == FLIGHT_NO * TIME * TIME
- 声明了四个常量,前三个是“访问器”,最后一个将一组非空航班信息映射到出发时间最长的航班信息。
CONSTANTS flight_no, flight_departure, flight_arrival, last_flight
- 然后将这些常量键入并定义为总函数。请注意,最后一个函数必须将非空集作为输入。在这里我使用了不同的方法来指定这些函数。一个是定义性的(具有等式),另一个是公理化的。
PROPERTIES // typing flight_no: FLIGHT_INFO --> FLIGHT_NO & flight_departure: FLIGHT_INFO --> TIME & flight_arrival: FLIGHT_INFO --> TIME & last_flight : POW1(FLIGHT_INFO) --> FLIGHT_INFO & // value flight_no = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | no) & flight_departure = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | dt) & flight_arrival = %(no, dt, at).(no |-> dt |-> at : FLIGHT_INFO | at) & !fs.(fs : POW1(FLIGHT_INFO) => last_flight(fs) : fs & !(fi).(fi : FLIGHT_INFO & fi : fs => flight_departure(fi) <= flight_departure(last_flight(fs)))
不隶属于 StackOverflow