AMN 和数学逻辑符号答案

【问题标题】：AMN and math logic notationAMN 和数学逻辑符号
【发布时间】：2009-12-12 13:46:02
【问题描述】：

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

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

【问题讨论】：

Stackoverflow 是这个问题的合适论坛，但形式方法问题（除了批评者可能表达对他们的厌恶的主观问题）在过去的。祝你好运...

标签： math requirements software-quality b-method

【解决方案1】：

你想get这样一个元素，还是测试你拥有的一个元素满足这个属性？我问是因为第二个似乎是手术的一个明智的先决条件。我不具体了解B-Method；我查看了一些文档，但找不到快速参考，所以这在某些细节上可能是错误的。

第二个应该是这样的（prj2 用于第二个投影）：

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

那么第一个就是：

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

【讨论】：

好吧，我想出了一个看起来像你的答案的解决方案。但是我在 AMN 中找不到投影功能，因为在实际问题航班中是八组（而不是三组）笛卡尔积的幂集的子集，因此很难编写...跨度>
我在我正在使用的软件（Atelier B）中找到了投影，但它仅用于关系。例如，如果我想访问第 4 个航班字段，我应该制作 prj2(prj2(prj2 flight) 吗？它是否像 lisp 中的列表一样工作？应该有一些更简单的方法来做到这一点 xD 我可以看看数组跨度>
实际上，我认为您应该考虑使用记录而不是数组。
我可以，但我从未听说过 AMN 上下文中的记录。
我以为我看到他们提到了，但我现在找不到了。

【解决方案2】：

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

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

和

对于所有 td、td'、td''，如果 td > td'' 并且 td' > td'' 则 td == td'

当然，这假设集合中只有一个元素。我无法确定 B 方法是否允许一阶逻辑的全部功能，但我认为您可以接近这一点。

【讨论】：

请注意，您甚至没有提到 flights 变量。
是的，一个很容易纠正的错误，但仍然是一个错误。我们大约在同一时间发布，当我看到你的时，我投了赞成票，因为它可能比我的更好。

【解决方案3】：

可以在 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)))

【讨论】：