AMN 和数学逻辑符号

Question

我不确定这是否适合 stackoverflow，但我不知道还能去哪里问。我正在研究 B 方法来证明需求规范的一致性，并且在指定操作的先决条件时，我对逻辑数学符号有疑问。

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

Answer 1

你想要_____吗 得到 这样的元素，或者 测试 您拥有的元素满足此属性吗？我这么问是因为第二个似乎是手术的合理先决条件。我不太了解B法的具体情况；我查看了一些文档，但找不到快速参考，因此这在某些细节上可能是错误的。

第二个应该看起来像这样（prj2 用于第二次投影）：

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

那么第一个是：

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

Answer 2

请原谅我的无知，我不熟悉的B-方法。但不能使用独特量词？它会是这个样子：

存在一个时间td，使得对于所有时间TD 'TD> TD'

和

对于所有TD，TD 'TD ''，如果TD> TD '' 和TD'> TD '' 然后TD TD =='

此，当然，假定有在该组恰好一个要素是。我真的不能告诉我们，如果B-方法允许一阶逻辑的全部力量，但是我认为你能来接近这个。

Answer 3

可以在 B 中定义函数。函数具有常量值，将在 ABSTRACT_CONSTANTS 子句中列出，并在 PROPERTIES 子句中定义。我尝试解释如何使用此结构来解决您的问题。

以下是一小段摘录

1. 介绍了给出航班信息的笛卡尔积的快捷方式；

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

2. 声明了四个常量，前三个是“访问器”，最后一个将一组非空航班信息映射到出发时间最长的航班信息。

CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight

3. 然后将这些常量键入并定义为总函数。请注意，最后一个函数必须将非空集作为输入。在这里我使用了不同的方法来指定这些函数。一个是定义性的（具有等式），另一个是公理化的。

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)))