Proving correctness in formal logic

Question

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?

Consider the following section of code involving integer variables:

if (i < j) {
    m = i;
} else {
    m = j;
}

By stating an appropriate output condition and then verifying the correctness of the piece of code, prove that after execution, m is equal to the minimum of i and j.

I have got the post condition as: {m = i ∧ i < j ∨ m = j ∧ j < i}

is this correct? and how do you verify this? It seems to simple.

Thanks.

Answer 1

Your post condition is correct. I personally find the following variant (which is equivalent) more natural though:

(i<j → m=i) ∧ (i≥j → m=j)

To prove that the program satisfies the post condition you do the following.

1. Note that to make sure the program always satisfies the post condition you should use true as your pre condition.

2. So you have the following Hoare triple:

   {true}
   if (i < j) {
   
   
       m = i;
   
   } else {
   
   
       m = j;
   
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

3. The postcondition needs to hold at the end of both branches, so (according to the standard weakest precondition rule for conditionals) we have

   {true}
   if (i < j) {
   
   
       m = i;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--.
   } else {                                       |
                                                  |
                                                  |
       m = j;                                     |   copy
       {(i < j → m = i) ∧ (i ≥ j → m = j)}     <--|
   }                                              |
   {(i < j → m = i) ∧ (i ≥ j → m = j)}  ----------'
   

4. Pushing the formula further up according to the weakest precondition for assignment yields

   {true}
   if (i < j) {
   
       {(i < j → i = i) ∧ (i ≥ j → i = j)}   <---.
       m = i;                                    | m replaced by i
       {(i < j → m = i) ∧ (i ≥ j → m = j)}   ----'
   } else {
   
       {(i < j → j = i) ∧ (i ≥ j → j = j)}   <---.
       m = j;                                    | m replaced by j
       {(i < j → m = i) ∧ (i ≥ j → m = j)}   ----'
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

5. At the top of the true branch we know that i < j, and at the top of the else branch we know that ¬(i < j):

   {true}
   if (i < j) {
       {i < j}                               (1)  <--- added
       {(i < j → i = i) ∧ (i ≥ j → i = j)}   (2)
       m = i;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}
   } else {
       {¬(i < j)}                            (3)  <--- added
       {(i < j → j = i) ∧ (i ≥ j → j = j)}   (4)
       m = j;
       {(i < j → m = i) ∧ (i ≥ j → m = j)}
   }
   {(i < j → m = i) ∧ (i ≥ j → m = j)}
   

6. What left to show is for any two consecutive assertions, the first assertions implies the second one. (These are usually referred to as "proof obligations".) We have two such obligations: (1) should imply (2) and (3) should imply (4). This is clearly the case.

   -- "qed" :-)