Exercise 3 from Microsoft's Dafny on Rise4Fun.com

dafny-exercise3

/*
 * Keeping the postconditions of Abs the same as above, change
 * the body of Abs to just y := x + 2. What precondition do you
 * need to annotate the method with in order for the verification
 * to go through? What precondition doe you need if the body is
 * y := x + 1? What does that precondition say about when you can
 * call the method?
 */
method Abs(x: int) returns (y: int)
   requires x == -1;
   ensures 0 <= y;
   ensures 0 <= x ==> x == y;
   ensures x < 0 ==> y == -x;
{
  y:= x + 2;
}

method Abs2(x: int) returns (y: int)
   requires x == -1; // no int value can satisfy this method
   ensures 0 <= y;
   ensures 0 <= x ==> x == y;
   ensures x < 0 ==> y == -x;
{
  y:= x + 1;
}

Hi, thanks a lot for your solution - I appreciate it. I was just wondering why we have kept the post-conditions related to when x is positive, when the function is not defined for that type of input anyway. It is only defined for negative input. What I am saying is, isn't the line "ensures 0 <= x ==> x == y;" redundant?