AMN和数学逻辑符号

我不确定这是适合的stackoverflow，但我不知道还有什么要问。我正在研究用于证明要求规范中一致性的B方法，并且在指定操作的前提条件时，我遇到了逻辑数学符号的问题。AMN和数学逻辑符号

简化原问题，我有一个变量，它是一个子集航班FLIGHT_NO×时间×时间之间的笛卡尔乘积，其中对于每个构件（无，TD，TA），绝不是飞行的数量 ，出发时间和到达时间。如何使用数学逻辑符号表示航班中具有最大td值的元素？

2009-12-12 webdreamer

**＃1 **是一个适当的论坛，这个问题，但是正式的方法问题（不是主观的那些批评者那里可以表达自己对他们的厌恶等）并非总是得到及时解答中过去。祝你好运... – 2009-12-12 13:56:52

你想获得这样的元素，或者测试一个元素必须满足这个属性？我在问，因为第二次似乎是手术的合理先决条件。我不明确B方法;我查看过一些文档，但找不到快速参考，因此在某些细节上可能会出错。

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

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

然后第一个是：

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

来源

2009-12-12 17:10:10

好吧，我想出了一个解决方案，看起来像你的答案。但我无法在AMN中找到投影功能，因为在实际问题中，航班是八套（而不是三套）笛卡尔积的一个子集，所以它使得它很难写... – webdreamer 2009-12-12 17:29:13

I我在我使用的软件（A工作室B）中发现了投影，但它仅用于关系。如果我想访问航班的第4个字段，我应该制作prj2（prj2（prj2航班）吗？它是否像列表中的lisp一样工作？应该有一些更简单的方法来做到这一点xD我可以看看阵列 – webdreamer 2009-12-12 17:46:10

实际上，我认为你应该考虑使用记录而不是阵列 – 2009-12-12 18:01:50

原谅我的无知，我不熟悉的B-方法。但是你不能使用唯一性量词吗？它会是这个样子：

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

和

所有TD，TD” TD'，如果TD > td''和td'> td''then td == td'

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

来源

2009-12-12 17:13:27

注意你甚至没有提及'航班'变数 – 2009-12-12 18:00:06

是的，这是一个容易纠正的错误，但仍然是一个错误。我们在同一时间张贴了一篇文章，当我看到你的时候，我提高了它，因为它可能比我好。 – 2009-12-12 18:22:20

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

来源

2017-06-29 11:47:17 dde

AMN和数学逻辑符号

回答

相关问题