vdm++ - 拡張暗黙関数定義における = と <=> の違い

Question

拡張された明示的な関数でいくつかの興味深い動作が見られます。

陰関数を定義する

  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 には、「ブール値を扱う場合、意味的に <=> と = は同等である」と記載されています。操作性に違いはありますか？