程序代写 􏰀 Loop Invariants (CLRS p.18-20)

􏰀 Loop Invariants (CLRS p.18-20)
This is not an easy topic for beginners. CLRS does not provide enough examples.
Topic 2: Correctness

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 0” — UNINFORMATIVE
􏰀 “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]
􏰀 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

Related Posts