proofformal-methodspost-conditionsproof-of-correctnesshoare-logic

Proving correctness of algorithm

I was wondering if anyone could help me answer this question. It is from a previous exam paper and I could do with knowing the answer ready for this years exam.

This question seems so simple that I am getting completely lost, what exactly is it asking for? Is the following algorithm to find maximum value correct? 

 {P: x≥0 ∧ y≥0 ∧ z≥0 } 
 if (x > y && x > z) 
 max = x; 
 else if (y > x && y > z) 
 max = y; 
 else 
 max = z; 
 {Q: max≥x ∧ max≥y ∧ max≥z ∧ ( max=x ∨ max=y ∨ max=z )}

The answer must be based on calculation of the weakest precondition for the algorithm.

How do you verify this? It seems to simple.

Thanks.

Solution

  • 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?