@function max3: int, int, int -> int

@axiom A1: all x,y,z: int. x>=y && x>=z ==> max3(x,y,z) = x
@axiom A2: all x,y,z: int. y>=x && y>=z ==> max3(x,y,z) = y
@axiom A3: all x,y,z: int. z>=x && z>=y ==> max3(x,y,z) = z


@requires true
@ensures m = max3(x,y,z)

@program
     @var x, y, z, m : int

     if (x >= y)  
        if (y >= z) 
	    m = x;
        else if (x >= z)
                 m = x
             else m = z;
     else if (y >= z)
                  m = y;
          else if (x >= z)
                  m = x
             else m = z;
@end
--