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


/* Returns the lesser of the two int arguments.
*/
ghost function Min(a: int, b: int): int 
  ensures Min(a,b) == a  ||  Min(a,b) == b
  ensures Min(a,b) <= a  &&  Min(a,b) <= b
{
  if a <= b then a
  else b
}

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

/* Returns the median of the three int arguments.
*/
ghost function Median(a: int, b: int, c: int): int
   ensures a == Median(a,b,c)  ||  b == Median(a,b,c)  ||  c == Median(a,b,c)
   ensures Min(a, Min(b,c)) <= Median(a,b,c) <= Max(a, Max(b,c))
{
   if a <= b then Max(a, Min(b,c))
   else Max(b, Min(a,c))
}


/* Returns the median of the three int arguments.
*/
method ComputeMedian(a: int, b: int, c: int) returns (median: int)
  ensures median == Median(a,b,c)
{
  // missing code!
}