AMN和数学逻辑符号表示法

Question

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

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

- webdreamer

---

Stackoverflow是一个适合这个问题的论坛，但是过去形式化方法的问题（除了主观的问题，反对者可以表达他们的厌恶）并不总是能够及时得到答复。祝好运... - Pascal Cuoq

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

- Alexey Romanov

---

好的，我想出了一个看起来和你的答案类似的解决方案。但是我在AMN中找不到投影功能，因为在实际问题中，航班是八个集合的笛卡尔积的幂集的子集（而不是三个），这使得编写变得非常困难... - webdreamer

我在使用Atelier B软件时发现了投影，但它只适用于关系。例如，如果我想访问航班的第四个字段，我应该制作prj2（prj2（prj2 flights））吗？ 它是否像Lisp中的列表一样工作？应该有一些更简单的方法来做这件事xD 我可能会看看数组。 - webdreamer

实际上，我认为你应该考虑使用记录而不是数组。 - Alexey Romanov

我可以翻译，但是我从未听说过在AMN上下文中的记录。 - webdreamer

我记得看到过它们的提及，但现在找不到了。 - Alexey Romanov

Answer 2

请原谅我的无知，我不熟悉B-Method。但是你不能使用唯一性量词吗？它看起来像：

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

和

对于所有的td、td'、td''，如果td > td''且td' > td''，那么td == td'

当然，这假设集合中恰好有一个元素。我无法确定B-Method是否允许完全使用一阶逻辑，但我认为你可以接近这个目标。

- Farley Knight

---

请注意，您甚至没有提到“flights”变量。 - Alexey Romanov

是的，这是一个容易纠正的错误，但仍然是个错误。我们差不多同时发布了帖子，当我看到你的时候，我点赞了，因为它可能比我的更好。 - Farley Knight

Answer 3

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

以下是一个小节选，其中

1. 引入了一个快捷方式，用于提供航班信息的笛卡尔积；

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

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

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

- dde