CONDITIONAL STATEMENT

if cond then S1; else S2; endif;

{Pre and cond}S1{Post},{Pre and not cond}S2{Post}
________________________________________________
{Pre} if cond then S1; else S2; end if;{Post}

EXAMPLE:

{true}
if x >= y then
max:=x;
else
max:=y;
end if
{(max = x or max = y) and
(max >= x and max >= y)}

We can use the proof rule to establish the two clauses
By combining the two clauses we obtain the Pre-condition.