Bottleneck in Hoare Logic unable to arrive at my {P} from {Q} {Q} = {n>0}
C1 = i := 1;
C2 = c := 1;
C3 = p := 0;
{P} = {i&lt;=n, p = fib(i-1), c = fib(i)}

My lack of understanding towards the rule of consequence in hoare logic is blocking me from find the solution which i hope someone can shed some light on how can i approach this with minimal abstraction of the process.

{R} = {i&lt;=n,p=fib(i-1),c=fib(i)[i\1]} i:= 1;{i&lt;=n, p = fib(i-1), c = fib(i)}

{R} = {1&lt;=n,p=fib(0),c=fib(1)}

{R} = {1&lt;=n,p=0,c=1}

{R1} = {1&lt;=n,p=0,c=1[c\1]}c:=1;{1&lt;=n,p=0,c=1}

{R1} = {1&lt;=n, p=0, true }

{R2} = {1&lt;=n,p=0[p\0]}p:=0;{1&lt;=n,p=0}

{R2} = {1&lt;=n,  true}{1&lt;=n,p=0}

{R2} = {1&lt;=n -> 0>x} :( i can't arrive at exactly n>0

*edit

From my observation the key problem is regardless of sequence i would always arrive at 1&lt;= n as not equivalent to n>0, i am not sure how i can legally perform P->P’  P’ C  Q’  Q’->Q to prove {P}C{Q}
You are doing it in the opposite order. You are starting with the postcondition
{i&lt;=n, p = fib(i-1), c = fib(i)} and then computing the precondition relative to the first assignment. You should instead use the last assignment, and go backwards:

{Q} = {n&gt;0}
{P3 = P2[i\1]} = {1&lt;=n, 0 = fib(1-1), 1 = fib(1)}
C1 = i := 1;
{P2 = P1[c\1]} = {i&lt;=n, 0 = fib(i-1), 1 = fib(i)}
C2 = c := 1;
{P1 = P[p\0]} = {i&lt;=n, 0 = fib(i-1), c = fib(i)}
C3 = p := 0;
{P} = {i&lt;=n, p = fib(i-1), c = fib(i)}


The steps above were computed bottom-up: you should read it in the same way.

It is then simple to check that Q and P3 are equivalent (assuming integer variables).