3

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

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

4

3 回答 3

4

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

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

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

那么第一个是：

flightWithGreatestTd = choice({flight | HasGreatestTd(flight)})
于 2009-12-12T17:10:10.960 回答
1

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

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

和

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

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

于 2009-12-12T17:13:27.950 回答
0

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

以下是一小段摘录，其中

  1. 介绍了给出航班信息的笛卡尔积的快捷方式；
DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME
  1. 声明了四个常量，前三个是“访问者”，最后一个将一组非空的航班信息映射到起飞时间最长的航班信息。
CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight
  1. 然后这些常量被输入并定义为总函数。请注意，最后一个函数必须将非空集作为输入。在这里，我使用了不同的方法来指定这些功能。一种是定义性的（具有等式），另一种是公理的。
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)))
于 2017-06-29T11:47:17.317 回答