Exercise 2 from Microsoft's Dafny on Rise4Fun.com

dafny-exercise2

/*
 * Using a precondition, change Abs to say it can only be
 * called on negative values. Simplify the body of Abs into
 * just one return statement and make sure the method still
 * verifies.
 */
method Abs(x: int) returns (y: int)
   requires 0 > x;
   ensures 0 <= y;
   ensures 0 <= x ==> x == y;
   ensures x < 0 ==> y == -x;
{
   return -x;
}