Thread: Hoare Logic Problems

Code:

------------------------------------------------ Assignment
{i = 5 /\ i + 2 = 7} a := i + 2 {i = 5 /\ a = 7}
------------------------------------------------ Consequence
     {i = 5 /\ a = 3} a := i + 2 {a = 7}

I'll look at the loop later.

for the first question, I 've learnt in a class that you should always start proving backwards, which means that I should replace the existing precondition with the postcondition first and in fact that's how I proved
{i = 5} a := i+2 {(a = 7) /\ (i=5)} (this was the first question for the tutorial and the above was the second question for the tutorial). Is it really okay to start from the precondition?

second I don't understand the assignment part ,

how can you direct change the postcondition a = 7 to (i = 5 /\ a = 7)?

Originally Posted by gomdohri

Prove {s = 2^i} while i < n do [i := i+1; s := s*2] {s = 2^i}

I tried to find an invariant but failed.

s = 2^i is the invariant.

Originally Posted by gomdohri

for the first question, I 've learnt in a class that you should always start proving backwards, which means that I should replace the existing precondition with the postcondition first and in fact that's how I proved
{i = 5} a := i+2 {(a = 7) /\ (i=5)} (this was the first question for the tutorial and the above was the second question for the tutorial). Is it really okay to start from the precondition?

It is indeed possible to take a piece of code with a given postcondition and invariants for each loop and construct the weakest precondition for this piece of code. If another precondition is given, you can verify if it implies the found weakest precondition and thus determine if it is sufficient to guarantee the given final postcondition. However, you can construct a derivation in any way that is convenient.

Originally Posted by gomdohri

second I don't understand the assignment part ,

how can you direct change the postcondition a = 7 to (i = 5 /\ a = 7)?

Do you have a problem with the consequence rule or with the assignment rule? The consequence rule works because i = 5 /\ a = 7 implies a = 7 (with regard to the postcondition) and i = 5 /\ a = 3 implies i = 5 /\ i + 2 = 7 (with regard to the precondition).

In the following code I used rule from the Wikipedia article about Hoare logic.

Code:

------------------------------------ Ass-t
{2s = 2^(i+1)} i := i + 1 {2s = 2^i}
------------------------------------ Cons ----------------------------- Ass-t
  {s = 2^i} i := i + 1 {2s = 2^i}         {2s = 2^i} s := 2*s {s = 2^i}
  --------------------------------------------------------------------- Comp-n
                {s = 2^i} i := i + 1; s = 2*s {s = 2^i}
             ------------------------------------------------ Cons
             {s = 2^i /\ i < n} i := i + 1; s = 2*s {s = 2^i}
      ----------------------------------------------------------------- While
      {s = 2^i} while i < n [i := i + 1; s = 2*s] {s = 2^i /\ ~(i < n)}
      ----------------------------------------------------------------- Cons
           {s = 2^i} while i < n [i := i + 1; s = 2*s] {s = 2^i}