Bottleneck in Hoare Logic unable to arrive at my {P} from {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).