Exercise 4 from Microsoft's Dafny on Rise4Fun.com

dafny-exercise4

/*
 * Write a function max that returns the larger of two given
 * integer parameters. Write a test method using an assert that
 * checks that your function is correct.
 */
function max(a: int, b: int): int 
{
   if a > b then a else b
}
method Testing() {
  assert max(10,12) == 12;
  assert max(12,10) == 12;
  assert max(10,10) == 10;
  assert max(-10,0) == 0;
}