This question seems so simple that I am getting completely lost, what exactly is it asking for?
The question is asking for you to formally prove that the program behaves as specified, by the rigorous application of a set of rules decided on in advance (as opposed to reading the program and saying that it obviously works).
How do you verify this?
The program is as follows:
if (x > y && x > z)
max = x;
else P1
with P1
a shorthand for if (y > x && y > z) max = y; else max = z;
So the program is basically an if-then-else. Hoare logic provides a rule for the if-then-else construct:
{B ∧ P} S {Q} , {¬B ∧ P } T {Q}
----------------------------------
{P} if B then S else T {Q}
Instanciating the general if-then-else rule for the program at hand:
{???} max = x; {Q} , {???} P1 {Q}
-------------------------------------------------------------------------------------
{true} if (x > y && x > z) max = x; else P1 {Q: max≥x ∧ max≥y ∧ max≥z ∧ ( max=x ∨ max=y ∨ max=z)}
Can you complete the ???
placeholders?