IF-THEN-ELSE Proof

 { PRE: x0 = x and y0 = y }

    if (x > y) then y := x

               else x := y

 { POST: x = y = max(x0,y0) }



 1) show { PRE and x > y } y := x { POST }
 2) show { PRE and ~(x > y) } x := y { POST }
 3) conclude  

    { PRE } if (x > y) then y := x
                       else x := y { POST }

    by IF-THEN-ELSE rule of inference

    QED