# Hoare Logic Problems

• Aug 17th 2012, 11:19 AM
gomdohri
Hoare Logic Problems
Hi, I have started studying Hoare Logic but I have two questions and I hope that you can help me with this.

First question is about Loops

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.

Second question is just about assignment statements but I am stuck

this time /\ is 'and'

Prove {(i = 5) /\ (a = 3)} a:= i +2 {a = 7}

thank you!
• Aug 17th 2012, 01:07 PM
emakarov
Re: 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.
• Aug 17th 2012, 05:20 PM
gomdohri
Re: Hoare Logic Problems
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)?
• Aug 18th 2012, 11:57 AM
emakarov
Re: Hoare Logic Problems
Quote:

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.

Quote:

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.

Quote:

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}```