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

^ = powered by

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!