Exercise 1 from Microsoft's Dafny on Rise4Fun.com

dafny-exercise1

/*
 * Write a test method that calls your Max method from
 * Exercise 0 and then asserts something about the result.
 */
method Max(a: int, b:int) returns (c: int)
ensures c >= a && c >= b;
ensures a > b ==> c == a;
ensures a <= b ==> c == b;
{
  if (a > b) {
    return a;
  }
  else {
    return b;
  }
}

method Testing() {
  var a := 10;
  var b := 12;
  var v := Max(a, b);
  assert v >= a && v >= b;
}