Loop Invariants (CLRS p.18-20)
This is not an easy topic for beginners. CLRS does not provide enough examples.
Topic 2: Correctness
Copyright By PowCoder代写 加微信 powcoder
Why Prove Correctness
Once you developed an algorithm, you at least need to show it does what it is supposed to do (and never errs!)
What is the difference between testing and proving?
To prove a program is correct, we start by wording correctness
Claim: For any instance I (satisfying ),
Algorithm-name(I) returns
E.g., For any two non-negative integers a and b, Multiply(a, b) returns the product a × b.
Topic 2: Loop Invariant
Basic Proofs
For simple statements, just reason with the effect of code (using logic).
procedure Swap(a,b) temp ← a
Claim: for any two pointers a and b, Swap(a, b) indeed assigns a the element that b pointed to originally, and assigns b the element that a pointed to originally.
Proof: Assume that initially a points to object x and b points to object y.
The first line creates a new pointer temp that also points to x. The second line sets a to point to y (just like b). Finally the last line sets b to point to the same object as temp, i.e. x. So, at the end of the execution, a points to y and b points to x, as required.
Topic 2: Loop Invariant
Proving Correctness using Loop Invariants
If a code is written using recursion, prove correctness using induction.
For code written using loops, prove correctness by the loop invariant method.
A loop-invariant is an assertion about the state of the code that is always true at the beginning of each loop-iteration.
Not any assertion, but an assertion that accurately describes the cumulative effect of repeatedly iterating through the loop; an assertion we can also use to prove the correctness of the code.
Topic 2: Loop Invariant
Proving Correctness using Loop Invariants (Cont’d)
Step 1: Identify the loop invariant
Q1: Do I understand what the loop does?
Q2: Do I understand the cumulative effect of the loop?
Q3: Can I word exactly the cumulative effect of the loop?
Step 2: Prove the loop invariant for
Initialization
Maintenance
Termination #1: Does the loop halt eventually? (CLRS does not
dicuss this; we added this property)
Termination #2: How do I prove correctness from the LI?
Topic 2: Loop Invariant
Step #1: Identifying and Rigorously Stating the Loop Invariant
Consider the code
procedure FindSum(A,n)
sum ← A[1] j←2
while (j ≤ n)
sum ← sum + A[j]
j←j+1 return sum
Let’s pick ”at the beginning” for the point of reference and ask: at the beginning of each loop iteation, what holds true, so that its being true throughout the loop implies the correctness of the procddure?
Let’s analyze: according to the code
whenj=2,(thevalueof)sum=A[1]
when j = 3, sum = A[1]+A[2]
whenj=kforanyk
“At the beginning of each loop iteration
sum = sumprevious iteration + A[j − 1]” — UNINFORMATIVE
To make sure you don’t mess with the indices — check it! Plug-in values of j like what was done above and check.
Step #2: Proving Loop Invariants
Once we have identified and stated the LI, it is time to prove it — and to use it to prove the correctness of the entire code.
Proving LI means proving the following 4 parts
Initialization: Does LI hold before the loop starts?
Maintenance: If LI holds at the beginning of j′-th iteration, does it hold also at the beginning of the (j′ + 1)-th iteration?
Termination #1: Does the loop terminate?
Termination #2: When the loop terminates, does it lead to the correctness of the overall algorithm / the claim we were making?
Step #2: Proving Loop Invariant
Our loop-invariant: “At the beginning of each loop iteration, j−1
sum = A[i]” i=1
Initially: Before the loop begins sum = A[1] = A[1, …, (2 − 1)]
Maintenance: Suppose that at the beginning of iteration j (the j−1
(j − 1)-th iteration), sum = A[i]. i=1
Then, at the beginning of iteration j + 1 (j-th iteration), sumafter =
j−1 before LI
jafter−1
A[i] + A[j] =
Termination #1: The loop terminates as we only increment j, so
Termination #2: When the while-loop terminates, j = n + 1, in which case the LI implies sum = ni=1 A[i].
eventually we would have j > n
Topic 2: Loop Invariant
More Loop Invariant Examples
procedure InsertionSort(A)
Topic 2: Loop Invariant
for (j from 2 to n)
key ← A[j] **insert A[j] into sorted sublist A[1..j − 1] i←j−1
while (i>0 and A[i]>key)
A[i + 1] ← A[i]
i←i−1 A[i + 1] ← key
More Loop Invariant Examples
To prove correctness – use two loop invariants, one nested inside another.
What is the loop invariant of the for-loop?
LI1: “At the beginning of each for-loop iteration A[1, …, j − 1]
contains the same elements that were there initially, only in order.”
Initialization: j = 2 and clearly A[1] is a sorted array of size 1.
Maintenance: TBD
Termination #1: We don’t alter j at the body of the loop + Termination of the while-loop (TBD)
Termination #2: When the loop terminates, j = n + 1 so A[1, …n] (which is the whole array) is sorted.
But how to prove maintenance?
Topic 2: Loop Invariant
More Loop Invariant Examples
To prove the maintenance property of the LI for the for-loop we actually use a LI for the while-loop
LI2: Let Abefore[1..j] denote the array before we started iterating through the while loop. Then at the beginning of each iteration of the while loop:
(i) A[1..i + 1] = Abefore[1..i + 1]
(ii)A[i + 2..j] = Abefore[i + 1..j − 1]
Initialization / maintenance / termination #1 of LI2: HW
Topic 2: Loop Invariant
More Loop Invariant Examples
To prove the maintenance property of the LI for the for-loop we actually use a LI for the while-loop
LI2: Let Abefore[1..j] denote the array before we started iterating through the while loop. Then at the beginning of each iteration of the while loop: (i) A[1..i + 1] = Abefore[1..i + 1]
(ii)A[i + 2..j] = Abefore[i + 1..j − 1]
The termination #2 of LI2 is how to derive the maintenance property of LI from the termination of the while-loop.
Termination #2: At the end of while loop, i is the largest entry in {1, 2, 3, …, j − 1} for which A[i] ≤ key (or 0, if no such entry exists). So LI2 together with putting key at A[i + 1], we have that
A[1, ..j] = Abefore[1, .., i], key, Abefore[i + 1, .., j − 1]
As Abefore[1, ..j − 1] was sorted & by definition of i ⇒ A[1, ..j] is sorted.
Topic 2: Loop Invariant
Loop invariant vs. Mathematical induction
Arguing correctness
When recursion is involved, use induction
When loop is involved, use loop invariant (and induction)
Common points
initialization vs. base step
maintenance vs. inductive step
Difference
termination vs. infinite
Topic 2: Loop Invariant
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com