Difference between = and <=> in extended implicit function definition

Question

I see some interesting behaviour with an extended explicit function.

I define an implicit function

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

And a corresponding explicit function (since the post condition is computable)

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

isLeap2 returns values expected. Then I define an extended implicit function

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

This works as expected except when provided with an argument that is a multiple of 100 but not 400. The result is

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

Then as I was typing this in I thought, what about

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

and the result is as expected. What is the difference between '=' and '<=>' in this context? In section 3.1.1 of VDM-10 Language Manual (issue Nov 2014) is states "Semantically <=> and = are equivalent when we deal with boolean values." Are they different operationally?

Answer 1

The answer of course is operator precedence. If I parenthesise the first version all is well.

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