// SE 504  Spring 2026  HW #1
// Student Name: ...


/* Returns the greater of the two arguments.
*/
ghost function Max(a: int, b: int): int 
{
  if a < b then b 
  else a
}

/* Returns (in s and m, respectively) the sum and the
** maximum of the two arguments.
*/
method MaxSum(x: int, y: int) returns (s: int, m: int)
  ensures s == x+y
  ensures m == Max(x,y)
{
  s := x+y;
  if x < y { m := y; }
  else { m := x; }
}


/* Given the sum of two numbers and their maximum, returns the
** two numbers.
*/
method ReconstructFromMaxSum(s: int, m: int) returns (x: int, y: int)
  // Imposing a precondition is necessary to make it possible to 
  // satisfy the postcondition.
  requires true   // needs strengthening
  ensures s == x + y
  ensures m == Max(x,y)
{
  // Missing method body
}