Consider the program:

$//\{$N $>=0\}$ # P

i $=0$;

while $($i $<$ N$)\{$

$//[$I$]$ loop invariant

i $=$ i $+1$;

$\}$

$//\{$i $==$ N$\}$ # Q

The while loop is the same as

while $($true$)\{$

$//[$I$]$ loop invariant

If $(!($i $<$ N$)$ break;

i $=$ i $+1$;

$\}$

Using a sufficiently strong invariant to prove the program is correct,

Let $[$I$]=$ i $<=$ N$,$ we want to find that eventually P $($ which is N$>=0)$ implies our WP

WP$([$i :$=0$; while $[$i $<=$ N$]$ i $<$ N do i :$=$ i $+1],$ i $=$ N$)$

$=$ WP$($i :$=0$; WP$($while $[$i $<=$ N$]$ i $<$ N do i:$=$ i $+1],$i $=$ N$))$

Prove inner WP $($ a loop$)$ with three rules and then combining them

I : the loop invariant $($should hold when entering the loop$)$

$($I & b$)=>$ WP$($S$,$ I$)$ : $($entering the loop because b is true$)$ I is preserved after each loop body execution

$($I & $!$b$)=>$ Q $($exiting the loop because b is false$),$ when exiting the loop, the post condition holds

$1.[$I$]$

$=($i $<=$ N$)$

$2.($I & b$)=>$ WP$($S$,$ I$)$

$=($i $<=$ N & i $<$ N$)=>$ WP$($i :$=$ i $+1,$ i $<=$ N$)$

$=($i $<$ N$)=>$ WP$($i :$=$ i $+1,$ i $<=$ N$)$

$=($i $<$ N$)=>$ i $+1<=$ N

$=($i $<$ N$)=>($i $<=$ N $-1)$

$=!($i $<$ N$)||($i $<=$ N $-1)$

$=($i $>=$ N $||($i $<$ N$)$

$=$ True

$3.($I & $!$b$)=>$ Q

$=($i $<=$ N & $(!$i $<$ N$))=>($i $=$ N$)$

$=($i $<=$ N & i $>=$ N$)=>($i $=$ N$)$

$=($i $=$ N$)=>($i $=$ N$)$

$=$ True

Combine to make $($i $<=$ N & True & True$)$

$=$ i $<=$ N

$=$ WP$($i:$=0$; i $<=$ N$)$

$=0<=$ N

$=$ P

Since the WP results in P and P $=>$ P is a tautology then we know the program satisfies the preconditions.

Attempt to prove the program using an insufficiently strong invariant, describe what happens and why.