/*@ ensures
@ \result >= x && \result >= y &&
@ \forall int z; z >= x && z >= y => z >= \result
@*/
int max(int x, int y) {
if (x > y) return x; else return y;
}
/*@ ensures
@ \result >= x && \result >= y &&
@ \forall int z; z >= x && z >= y => z >= \result
@*/
int max(int x, int y) {
if (x > y) return x; else return y;
}
::
::
::
