pub open spec fn max(x: int, y: int) -> int
{ if x >= y { x } else { y } }
This function computes the maximum of two given integers.