Error in specification for Height_Valid

[ahuoguo]

Hi Richard,

In the Height_Valid predicate:

  predicate Height_Valid() 
    reads this, Repr 
  {
    Valid() &&
    (left == null && right == null) ==> height == -1 &&
    (left != null && right == null) ==> height == left.height + 1 &&
    (left == null && right != null) ==> height == right.height + 1 &&
    (left != null && right != null) ==> height == max(left.height, right.height) + 1 &&
    (right != null) ==> right.Height_Valid() &&
    (left != null) ==> left.Height_Valid()
  }

since && has higher precedence than ==>, it's actually different from the following

    ghost predicate Height_Valid()
      reads this, Repr
    {
      && Valid()
      && ((left == null && right == null) ==> height == 0)
      && ((right != null) ==> right.Height_Valid())
      && ((left != null) ==> left.Height_Valid())
      && ((left != null && right == null) ==> height == left.height + 1)
      && ((left == null && right != null) ==> height == right.height + 1)
      && ((left != null && right != null) ==> height == max(left.height, right.height) + 1)
    }

which I believe was your intended specification