Program Correctness William Groesbeck, Sam Delaney

Program Correctness William Groesbeck, Sam Delaney

Program Correctness What is program correctness?

Program Correctness What is program correctness? A program is said to be correct if it produces the correct output for every possible input

Program Correctness Two types of correctness: Total – algorithm always returns at least one correct solution Partial – if a solution is returned, it will be correct

Program Correctness Tony Hoare – Introduced the idea of partial correctness Also the creator of the quick sort – one of the most commonly used and studied sorting algorithms

Program Correctness Partial correctness with respect to assertions: A program can be partially correct with respect to the initial assertion (represented with p) and the final assertion (represented by q). Notation: p{S}q – Hoare triple

Program Correctness Example 1, Section 4.5: Show that the program segment y : 2, z : x y is correct with respect to the initial assertion p: x 1 and the final assertion q: z 3

Program Correctness Solution: Suppose that p is true, so x 1. According to the program segment, y is then assigned 2. Then z is assigned x y, or 1 2 making z 3. Thus, S is correct with respect to both the initial and the final assertions. p{S}q is true.

Program Correctness Example 2: int identity(int x){ x x*1; return x; }

Program Correctness Curry-Howard Correspondence Deep result in proof theory that states that a proof of functional correctness in constructive logic corresponds to a certain program in the lambda calculus Converting a proof in this way is called program extraction.

Program Correctness Lambda Calculus: Formal system designed to investigate function definition Greatly influenced functional programming language including Lisp, ML, and Haskell Consists of a single variable substitution and a single function definition scheme. Undecidability

Program Correctness Lambda Calculus Expressions f(x) x 2 λ x. x 2 f(3) (λ x. x 2) 3 (λ f. f 3)(λ x. x 2) (λ x. x 2)3 3 2 5

Program Correctness Example 2 (Revised): int identity(int x){ x x*2; return x; } (λ x. x*2)

Program Correctness Example 3 : int identity(int x){ x x*2; return x; } (λ x. x*2) If x 3? (λ f. f 3) (λ x. x*2)

Program Correctness Conclusion: Partial / Total Correctness Tony Hoare Partial correctness with respect to Curry-Howard Correspondence Lambda Calculus Bonus! Name two things that Tony Hoare was best known for

Program Correctness Questions?