To prove something about an imperative program, you need to devise statements called assertions to go with the program. For example, to prove that the program Fact(n) returns the factorial of n, abbreviated n!, we need to assume the assertion n≥1 at the beginning and make the assertion Fact = n! at the end.
We also need a creative step: an assertion of a loop invariant stating something that is true before the test of any while loop. In this case it is:
1<k≤n+1 && Fact == (k-1)!
Then we decorate the program with these assertions, shown in red:
1≤n
Fact = 1
let k = 2
1<k≤n+1 && Fact == (k-1)!
while (k ≤ n) {
Fact = Fact * k
k = k+1
}
Fact == n!
Hoare devised rules that summarize the effect of each type of program statement. They can be applied mechanically to transform the decorated program with the eventual goal of eliminating all the assertions.
The rule for while loops is:
LI LI LI
while(B){ C} can be rewritten as while (B) {
LI && B
C
LI
}
LI && !B
In words: LI (the Loop Invariant) must be true before the while loop is entered. When B is true, executing C must preserve the truth of LI. And if B is not true, LI && !B will be true after the closing }.
The rule for let statements and assignments is simpler.
let v = E can be rewritten as Q(E)
Q(v) let v = E
v = E can be rewritten as Q(E)
Q(v) v = E
In words: to prove that Q(v) is true after v=E executes, you must prove Q(E) is true before it is executed.
Another rule allows us to combine adjacent assertions:
Q can be rewritten as Q implies R
R
Finally, any assertion that can be proved true by itself can be eliminated.
Applying these rules repeatedly to the Fact program generates many intermediate assertions leaving just the ones in red. The ones that have disappeared are shown in blue.
1≤n implies 2≤n+1 && 1==1!
let Fact= 1
2≤n+1 && Fact == 1!
let k = 2
1<k≤n+1 && Fact == (k-1)!
while (k ≤ n) {
1<k≤n+1 && Fact == (k-1)! && k≤n
implies 0<k≤n && Fact*k == k!
0<k≤n && Fact*k == k!
Fact = Fact * k
0<k≤n && Fact == k!
k = k+1
1<k≤n+1 && Fact == (k-1)!
}
1<k≤n+1 && Fact==(k-1)! && k>n implies Fact==n!
Fact = n!
Each red statement is easily proved.
In contrast, there is nothing to prove about the LISP version since it is virtually the definition of Facorial(n) Also Hoare’s method doesn’t prove that Fact always halts if n≥1, but that seems obvious too.
Now consider MiniMatch from the KMP section.
function MiniMatch(Q, i, j) {
P[j]==Q[i] ? j
: j==1 ? 0
: MiniMatch(Q, i, L(j-1)+1)
}
Here is the imperative function:
function MM(Q, i, j) {
while (P[j]!=Q[i] && j!=1) {
j = L(j-1)+1
}
return P[j]==Q[i] ? j+1 : 0}
Theorem 1. MM(Q, i, j) = MiniMatch(Q, i, j)
Proof: Decorate MM with assertions.
function MM(Q, i, j) {
j≥1
while (P[j]!==Q[i] && j!=1){
j = L(j-1)+1
}
return P[j] == Q[i] ? j+1 : 0
MiniMatch(Q,i,j)==(P[j]==Q[i])?j+1 :0)
}
Applying Hoare’s method, the decorated program becomes:
function MM(Q, i, j) {
j≥1 && L(j)≥0 (X)
while (P[j]!=Q[i] && j!=1) {
j≥1 && L(j)≥0 && P[j]!=Q[i] && j!=1
implies L(j-1)+1≥1 && L(L(j-1)+1)≥0 (Y)
L(j-1)+1 ≥1 && L(L(j-1)+1)≥0
j = L(j-1)+1
j≥1 && L(j)≥0
}
j≥1 && L(j)≥0 && (P[j]=Q[i] || j=1)
implies
(P[j]==T[i]?j+1:0)==MiniMatch(Q,i,j) (Z)
return P[j] = T[i] ? j+1 : 0
MiniMatch(T,i,j)==(P[j]==T[i] ? j+1 :0)
}
X can’t be proven so is simply a precondition for calling MM. Y is obvious from the arithmetic. By the properties of L, Z becomes:
j≥1 && L(j)≥0 && (P[j]==Q[i] || j==1)
implies
(P[j]==Q[i] ? j+1 : 0)=(P[j]==Q[i]?j+1 : …)
which is also obvious.
We also need to prove that the loop always terminates, and that is the only reason we created the loop invariant j≥1 && L(j)≥0. From those initial conditions and Theorem 1 from the KMP section, which proved L(j)<j, we see that j starts off ≥1 and decreases at every change until reaching 1.
QED
Here is MakeL, the function that fills in the LTable, decorated with the assertion needed to prove it works.
function MakeL(){
LTable[1] = 0
let j = 1
let i = 2
i>1 && j == L(i-1) +1 && for 1≤k<i, LTable[k] == L(k)
while i ≤ P.length {
if (P[j] == P[i]) {
LTable[i] = j
i = i+1
j = j+1
} else if (j==1) {
LTable[i] = 0
i = i+1
} else j = LTable[j-1]+1
}
for 1≤k≤P.length, LTable[k] == L(k)
}
Three more of Hoare’s rules for conditional statements are needed to check it.
Two are for conditional statements:
if (B) { if (B) {
C C
} else { can be replaced by Q
D } else {
} .. D
Q Q
}
if (B) { (B implies Q’) & (~B implies Q'')
Q’ if (B) {
C C
} else { can be replaced by } else {
Q’’ D
D }
}
The third rule is for assignments to array elements:
A[v] = E can be replaced by Q(Q(A’) where A’[i]=(i==v ? E : A[i])
Q(A) A[v] = E
Applying these rules eventually produces this decorated program:
function MakeL(){
1==1 && 0==0
LTable[1] = 0
1==L(1)+1 && Table[1] == L(1)
j = 1
2>1 && j == L(1) +1 && Table[1] == L(1)
i = 2
i>1&&j==L(i-1)+1 && for 1≤k<i,LTable[k]==L(k)
while (i < P.length) {
i>1 && j== L(i-1)+1 && for 1≤k<i,
LTable[k] == L(k) && i < P.length
if P[j] == P[i] {
i>0 && j== L(i) && for 1≤k≤i, LTable’[k] == L(k)
where LTable’[k] == (k == i ? j : LTable[k])
LTable[i] = j
i+1>1 && j == L(i) && for 1≤k<i+1,LTable[k]==L(k)
i = i+1
i>1 && j == L(i-1) && for 1≤k<i, LTable[k]==L(k)
j = j+1
i>1 && j=L(i-1) +1 && for 1≤k<i, LTable[k] =L(k)
} else if (j==1) {
i+1 > 1 && j == L(i)+1
&& for 1≤k<i+1, LTable’[k] == L(k)
where LTable’[k] == (k==i ? 0 : qLTable[k])
LTable[i] = 0
i+1>1 && j==L(i)+1 && for 1≤k<i+1, LTable[k]==L(k)
i = i+1
i>1 && j==L(i-1)+1 && for 1≤k<i, LTable[k] == L(k)
} else {
i>1 && LTable[j-1]+1 == L(i -1)+1
&& for 1≤k<i, LTable[k] == L(k)
j = LTable[j-1]+1
i>1 && j==L(i-1)+1 && for 1≤k<i, LTable[k] == L(k)
}
}
i>1 && j== L(i-1) +1 && for 1≤k<i, LTable[k] == L(k)
&& i≥P.length
implies
1≤k≤P.length, LTable[k] == L(k)
}
The first and last assertions are obvious.
To prove the three parts of the conditional assume i>1 && j==(i-1)+1
&& for 1≤k<i, LTable[k]==L(k) && i<P.length,
so L(i) == MiniMatch(P, i, L(i-1)+1)
Consider each of the clauses of the conditional structure.
Case 1: P[j]==P[i]
L(i) == MiniMatch(P, i, L(i-1)+1) == L(i-1)+1 == j
&& LTable’[k] == if k == i then L(i) else LTable[k],
so for 1≤k≤i, LTable’[k] == L(k)
Case 2: P[j]!=P[i] && j==1
L(i) == MiniMatch(P, i, L(i-1)+1) == L(i-1)+1 == 0
&& LTable’[k] == if k == i then 0 else LTable[k],
so for 1≤k≤i, LTable’[k] == L(k)
Case 3: P[j]!=P[i] && j!=1
j-1<i so LTable[j-1]==L(j-1)
along with 1≤k<i, LTable[k] == L(k)
So MakeL performs properly.
While the manipulations required by Hoare’s rules are tedious, it should be remembered that they can be carried out by a computer.