扩展隐式函数定义中 = 和 <=> 的区别答案

【问题标题】：Difference between = and <=> in extended implicit function definition扩展隐式函数定义中 = 和 <=> 的区别
【发布时间】：2016-02-12 06:24:50
【问题描述】：

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

我定义了一个隐式函数

  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 节中声明“当我们处理布尔值时，语义上和 = 是等价的”。它们在操作上是否不同？

【问题讨论】：

标签： vdm++

【解决方案1】：

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

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

【讨论】：