Finding the Maximum

A procedure that finds the maximum of two values is specified as follows:

     PROCEDURE Max(x,y,z:T)
          z:=z' |  z' = max x y        <--

As a first step, we introduce an IF-statement whose guard compares x and y:

     IF x > y
     THEN
          { x > y }  z:=z' |  z' = max x y       <--
     ELSE
          { x <= y } z:=z' |  z' = max x y
     FI    

Proceeding with the first branch, clearly we can show:

  x > y  ==>  max x y = x

Thus we can weaken the assertion:

{ max x y = x } z:=z' | z' = max x y

then rewrite the highlighted expression:

     z:=z' |  z' = x

and introduce an assignment:

     z := x

Similarly the second branch can be refined to:

     z := y

Gathering the refined components together, we get:

     PROCEDURE Max(x,y,z:T)
     IF x > y
     THEN
          z := x
     ELSE
          z := y
     FI