// Dafny
// limbaj functional
function max(a : int, b : int) : int
{
  if (a > b) then
    a
  else
    b
}

// limbaj imperativ
method computeMax1(x : int, y : int) returns (r : int)
  ensures r == max(x, y)
{
  if (x > y) {
    r := x;
  } else {
    r := y;
  }
}

method computeMax2(x : int, y : int) returns (r : int)
  ensures r >= x && r >= y
  ensures r == x || r == y
{
  if (x > y) {
    r := x;
  } else {
    r := y;
  }
}