Correctness and Termination Proofs
Copyright © 2018 by . All Rights Reserved.
Learning Outcomes
Copyright By PowCoder代写 加微信 powcoder
by the End of the Lecture, Students that Complete
the Recommended Exercises should be Able to:
Contrast Proof with White-Box and Black-Box Testing Contrast Partial and Total Correctness Describe Termination and the use of Rank Functions Describe Structural Induction
Copyright © 2018 by . All Rights Reserved.
Reading and Suggested Exercises
Copyright © 2018 by . All Rights Reserved.
Read the following Chapter(s): None
Alan Turing proved that it is Impossible
to Create an Algorithm that will Determine if a Program will Terminate on a Certain Input (this is known as the “Halting Problem”)
Testing provides Confidence in the Correctness of a Program and testing Techniques can be Divided into Black-Box and White-Box Testing
Copyright © 2018 by . All Rights Reserved.
Program Testing
White-Box Testing is Characterized by Examining Internal Structure and Testing each Logical Case
this Approach is frequently Infeasible
(e.g., 𝒏 Branching Statements entails 𝟐𝒏 Combinations)
Copyright © 2018 by . All Rights Reserved.
Program Testing
White-Box Testing is Analogous to using Perfect Information about a Device to Ensure that Every Possibility is Tested
Program Testing
Copyright © 2018 by . All Rights Reserved.
Black-Box Testing is Characterized by Testing Programs Without Observing Internal Structure
this Approach Compares the Results on Problem Instances for which the Correct Result is Known
Copyright © 2018 by . All Rights Reserved.
Program Testing
Black-Box Testing is Analogous to Testing a Device by Using it, and Entails Testing Three Input Classes: “Good”, “Bad”, and “Ugly”
Copyright © 2018 by . All Rights Reserved.
Program Testing
Black-Box Testing is Analogous to Testing a Device by Using it, and Entails Testing Three Input Classes: “Good”, “Bad”, and “Ugly”
the “Good” the “Bad” the “Ugly” Copyright © 2018 by . All Rights Reserved.
Program Testing
I have included this image in case you thought the analogy of someone trying to toast a croissant in an automatic toaster was too contrived…
https://www.wikihow.com/Heat-Croissants
Program Testing
Copyright © 2018 by . All Rights Reserved.
Partial and Total Correctness
Testing Can Indicate the Presence of Problems, but it Cannot Demonstrate the Absence of Problems
Proofs of Correctness, on the other hand, are Formal Proofs that Programs are Free of Problems
Copyright © 2018 by . All Rights Reserved.
Partial and Total Correctness to Prove that a Function is Totally Correct
you must Prove that:
the Function Terminates whenever the Input is Valid
this is known as “Termination”
If the Function Terminates, Then the Result is Correct
this is known as “Partial Correctness” Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
Can you Guarantee that this Function Terminates? Why or Why Not?
fact :: Integer -> Integer
| (n == 0) = 1
| (n > 0) = n * (fact (n-1))
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
to Prove that Recursive Function 𝑓 Terminates, Devise a Rank Function that Maps Each Input onto a Nonnegative Integer…
…and then Prove that:
If function 𝒇 is passed an Argument of Rank 𝑘 Then Rank 𝑘 must be Greater Than the Rank of the Argument passed to Each Subsequent Recursive Call
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
How could you Determine a Suitable Rank Function for zip?
zip :: [a] -> [b] -> [(a, b)]
zip (h1:t1) (h2:t2) = (h1,h2) : zip (t1 t2)
zip _ _ = []
n.b., each input to zip is two list arguments, so rank :: [a] -> [b] -> Integer
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
What are the Arguments that will be Passed to Each Call to zip in the Following Evaluation?
zip [1, 3, 25] [‘a’, ‘c’, ‘y’, ‘z’]
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
zip [1, 3, 25] [‘a’, ‘c’, ‘y’, ‘z’]
will make the Recursive Call zip [3, 25] [‘c’, ‘y’, ‘z’]
will make the Recursive Call zip [25] [‘y’, ‘z’]
will make the Recursive Call zip [] [‘z’]
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
Now Suppose
rank [1, 3, 25] [‘a’, ‘c’, ‘y’, ‘z’] = 𝒓𝒂𝒏𝒌𝟏 rank [3, 25] [‘c’, ‘y’, ‘z’] = 𝒓𝒂𝒏𝒌𝟐 rank [25] [‘y’, ‘z’] = 𝒓𝒂𝒏𝒌𝟑
rank [] [‘z’] = 𝒓𝒂𝒏𝒌𝟒
What Function could you use that would Guarantee 𝒓𝒂𝒏𝒌𝟏 > 𝒓𝒂𝒏𝒌𝟐 > 𝒓𝒂𝒏𝒌𝟑 > 𝒓𝒂𝒏𝒌𝟒 ?
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
Consider the Function Definition
rank list1 list2 = min (length list 1) (length list 2)
rank [1, 3, 25] [‘a’, ‘c’, ‘y’, ‘z’] rank [3, 25] [‘c’, ‘y’, ‘z’] rank [25] [‘y’, ‘z’]
rank [] [‘z’]
Can you Prove this rank Function Definition will work in the General Case?
Copyright © 2018 by . All Rights Reserved.
= 3 = 2 = 1 = 0
Formal Proofs of Termination
zip (h1:t1) (h2:t2) = (h1,h2) : zip (t1 t2)
What is the Rank of the Arguments?
What is the Rank of the Recursive Arguments? Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
zip (h1:t1) (h2:t2) = (h1,h2) : zip (t1 t2)
What is the Rank of the Arguments? min(length(h1 : t1), length(h2 : t2))
= min(1 + length(t1), 1 + length(t2))
What is the Rank of the Recursive Arguments? min(length(t1), length(t2))
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
How do you Prove min(1 + length(t1), 1 + length(t2)) is Greater than min(length(t1), length(t2)) ?
n.b., you can use a proof by exhaustion (i.e., proof by cases) to accomplish this easily
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
Prove min(1 + length(t1), 1 + length(t2)) is Greater than min(length(t1), length(t2))
Case 1: length(t1) > length(t2)
min(1 + length(t1), 1 + length(t2)) = 1 + length(t2)
> length(t2)
= min(length(t1), length(t2))
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Termination
Prove min(1 + length(t1), 1 + length(t2)) is Greater than min(length(t1), length(t2))
Case 2: length(t1) ≤ length(t2)
min(1 + length(t1), 1 + length(t2)) = 1 + length(t1)
> length(t1)
= min(length(t1), length(t2))
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness a Function that Oberves the Constraints of
Primitive Recursive will always have Termination
it follows that, in order to Demonstrate that Primitive Recursive Function 𝒇 is Totally Correct, you Need only Demonstrate that 𝒇 is Partially Correct
i.e., “If 𝑓 Terminates Then the Result was Correct” Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness
Demonstrating Partial Correctness is the Proof of an Implication Statement, so typically Structural Induction is Necessary
Structural Induction requires Assumptions that Lists are of Finite Length and that Functions are Defined over all Possible Inputs
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness to Prove that a Property 𝑃 holds for
All Finite Lists using Structural Induction: Prove the Property Holds for the Base Case
i.e., 𝑃 = 𝑇𝑟𝑢𝑒
Then Prove that, Under the Assumption 𝑃 𝑥 = 𝑇𝑟𝑢𝑒,
the Claim 𝑃 𝑦 ∶ 𝑥 = 𝑇𝑟𝑢𝑒 Holds as well
the Assumption is the Induction Hypothesis Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness
How would you Write a Function (or functions) that Computes the Sum of the Doubling of a List?
doubleList :: [Int] -> [Int]
sumList :: [Int] -> Int
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness
doubleList :: [Int] -> [Int]
doubleList [] = [] D1
doubleList (h:t) = 2*h : doubleList t D2 sumList :: [Int] -> Int
sumList [] = 0 S1 sumList (h:t) = h + sumList t S2
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness
How can you Prove (using Structural Induction) that sumList (doubleList x) Correctly Computes the Sum of the Doubling of a List?
also, What is the Rank Function? and, Do we Need such a Function to Prove
Total Correctness here? Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness
the Conjecture to be Proven here is that the Result is the Same as Twice the Sum of the List
i.e., Proving that this Works is (here) the Same As Proving sumList(doubleList x) = 2 * sumList x
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness to Prove this Using Structural Induction…
first Prove the Base Case… sumList(doubleList []) = 2 * sumList []
…then Assume… sumList(doubleList t) = 2 * sumList t
…in order To Prove… sumList(doubleList h:t) = 2 * sumList h:t
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness
Knowledge Base
sumList [] = 0
sumList (h:t) = h + sumList t
doubleList [] = []
doubleList (h:t) = 2*h : doubleList t
Prove: sumList(doubleList []) = 2 * sumList []
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness
Knowledge Base
sumList [] = 0
sumList (h:t) = h + sumList t
doubleList [] = []
doubleList (h:t) = 2*h : doubleList t
sumList(doubleList []) = 2 * sumList []
sumList([]) = 2 * sumList [] 0 = 2 * 0
Copyright © 2018 by . All Rights Reserved.
by D1 by S1
Formal Proofs of Correctness
Knowledge Base
sumList [] = 0
sumList (h:t) = h + sumList t
doubleList [] = []
doubleList (h:t) = 2*h : doubleList t
sumList(doubleList t) = 2 * sumList t
Prove: sumList(doubleList h:t) = 2 * sumList h:t
Copyright © 2018 by . All Rights Reserved.
Formal Proofs of Correctness
Knowledge Base
sumList [] = 0
sumList (h:t) = h + sumList t
doubleList [] = []
doubleList (h:t) = 2*h : doubleList t
sumList(doubleList t) = 2 * sumList t
sumList(doubleList h:t) = 2 * sumList h:t
sumList(2*h : doubleList t) = 2 * sumList h:t 2*h + sumList (doubleList t) = 2 * sumList h:t 2*h + (2 * sumList t) = 2 * sumList h:t 2*h + (2 * sumList t) = 2 * (h + sumList t) 2*h + (2 * sumList t) = 2*h + (2 * sumList t) Q.E.D.
Copyright © 2018 by . All Rights Reserved.
by D2 by S2 by IA by S2 by S2
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com