int min, max;

/* The following function saturates its input x between min and max,
   returning min if x is below min and max if x is above max.
   
   Q1: Formalize in the ACSL contract of saturation, 
   and then verify, the following informally expressed property:

   "saturation always returns a value comprised between min and max"

   Q2: The specification from Q1 is partial. Make the function more
   specified by formalizing and verifying the following property:

   "if x is comprized between min and max inclusive,
    then saturation returns x unchanged"

   Q3: Is the specification of saturation obtained so far complete?
   If you think that it is, prove it.
   If you think that it isn't, turn the specification of saturation 
   that you have built in Q1 and Q2 into a complete specification.
*/

/*@
  assigns \nothing;
*/
int saturation(int x)
{
  int res;
  if (x <= min) 
    res = min;
  else if (x >= max)
    res = max;
  else res = x;
  return res;
}