1

我看到一些带有扩展显式函数的有趣行为。

我定义了一个隐式函数

  isLeap (year:nat) res:bool
    post res = year rem 4 = 0 and (year rem 100 = 0 => year rem 400 = 0);

以及相应的显式函数（因为后置条件是可计算的）

  isLeap2 : nat -> bool
  isLeap2 (year) == year rem 4 = 0 and (year rem 100 = 0 => year rem 400 = 0);

isLeap2 返回预期值。然后我定义了一个扩展的隐式函数

  isLeap (year:nat) res:bool
    == year rem 4 = 0 and (year rem 100 = 0 => year rem 400 = 0)
    post res = year rem 4 = 0 and (year rem 100 = 0 => year rem 400 = 0);

这可以按预期工作，除非提供的参数是 100 但不是 400 的倍数。结果是

Error 4056: Postcondition failure: post_isLeap in 'test' (/Users/paul/Documents/Overture/workspace/test/test.vdmsl) at line 8:31

然后当我输入这个时，我想，怎么样

  isLeap (year:nat) res:bool
    == year rem 4 = 0 and (year rem 100 = 0 => year rem 400 = 0)
    post res <=> year rem 4 = 0 and (year rem 100 = 0 => year rem 400 = 0);

结果和预期的一样。在这种情况下，“=”和“<=>”有什么区别？在 VDM-10 语言手册（2014 年 11 月发行）的第 3.1.1 节中，声明“当我们处理布尔值时，语义上 <=> 和 = 是等价的”。它们在操作上是否不同？

4

1 回答 1

0

答案当然是运算符优先级。如果我给第一个版本加上括号，一切都很好。

post res = (year rem 4 = 0 and (year rem 100 = 0 => year rem 400 = 0))；

于 2016-02-12T06:41:43.257 回答