Transcript Program Correctness

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?