Proving correctness of an iterative Fibonacci algorithm
The condition $a \leq b$ is a loop invariant, but it captures very little of the operation of the loop. A better loop invariant is
$$ a = F_{i-2} \text{ and } b = F_{i-1}. $$
This clearly holds just before the loop. The loop sets $a' = b = F_{i-1}$, $b' = a+b = F_{i-2}+F_{i-1}=F_i$, $i' = i+1$, from which it is easy to prove that it maintains the loop invariant. When the loop has finished, we must have $i = n+1$, and so $a = F_{i-2} = F_{n-1}$ and $b = F_{i-1} = F_n$.

There is a weak point in this argument: How do we know that $i = n+1$ at the end of the loop? We can fix this by strengthening the loop invariant to
$$ a = F_{i-2} \text{ and } b = F_{i-1} \text{ and } i \leq n+1. $$
This holds just before the loop since $n \geq 1$ (assuming $n \geq 0$, a precondition that needs to be added to the entire function). It is maintained during the loop since at the beginning of each iteration $i \leq n$. Finally, after the loop we have $i \leq n+1$ and $i &gt; n$, which forces $i = n+1$ since $i$ is an integer.