AMN 和数学逻辑符号

发布于 2024-08-14 06:21:42 字数 261 浏览 13 评论 0原文

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

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

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

执妄 2024-08-21 06:21:42

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

第二个应该如下所示（prj2 用于第二个投影）：

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

那么第一个是：

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

Do you want to get such an element, or to test that an element you have satisfies this property? I am asking because the second seems a sensible precondition to an operation. I don't know the B-Method specifically; I've looked at some documents, but can't find a quick reference, so this may be wrong in some details.

The second should look like this (prj2 is used for the second projection):

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

Then the first is:

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

回复收藏 0 原文

拿命拼未来 2024-08-21 06:21:42

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

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

以及

对于所有 td、td'、td''，如果 td > td''和td'> td'' then td == td'

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

回复收藏 0 原文

因为看清所以看轻 2024-08-21 06:21:42

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

接下来是一小段摘录，其中

介绍了提供航班信息的笛卡尔积的快捷方式；

定义
    FLIGHT_INFO == FLIGHT_NO * 时间 * 时间

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

<前><代码>常量
航班编号、出发航班、到达航班、最后航班

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

<前><代码>属性
// 打字
航班号：FLIGHT_INFO --> FLIGHT_NO & 航班号
航班出发：FLIGHT_INFO -->时间与时间
航班到达：FLIGHT_INFO -->时间与时间
最后一次飞行：POW1(FLIGHT_INFO) --> FLIGHT_INFO 和
// 价值
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 =>
航班出发（fi）<=航班出发（最后一个航班（fs）））

It is possible to define functions in B. Functions have constant values and are to be listed in the ABSTRACT_CONSTANTS clause, and defined in the PROPERTIES clause. I try to explain how you can use this construct to solve your problem.

Follows a small excerpt where

a shortcut for the cartesian product giving flight information is introduced;

DEFINITIONS
    FLIGHT_INFO == FLIGHT_NO * TIME * TIME

four constants are declared, the first three are "accessors", and the last maps a non-empty set of flight informations to the flight information with the largest departure time.

CONSTANTS
    flight_no, flight_departure, flight_arrival, last_flight

Then these constants are typed and defined as total functions. Note that the last function must take as input a non-empty set. Here I used to different approaches to specify these functions. One is definitional (with an equality), and the other is axiomatic.

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

回复收藏 0 原文

~没有更多了~