Exercise 0 from Microsoft's Dafny tutorial on Rise4Fun.com

dafny-exercise0

/*
 * Write a method Max that takes two integer parameters and returns
 * their maximum. Add appropriate annotations and make sure  your code
 * verifies.
 */
method Max(a: int, b:int) returns (c: int)
  ensures c >= a && c >= b;
{
  if (a > b) {
    return a;
  }
  else {
    return b;
  }
}