Transcript Program Correctness

Section 3.6
Program Correctness
1
Program Correctness
• A correct program is a program that always
produces correct output
• It is easy to prove that a program is
incorrect:
– test program with sample input
– if it produces incorrect results, it is incorrect
• The converse is not so simple, however:
can’t prove correctness by testing unless all
possible inputs can be tested
2
Proving Program Correctness
• Also known as program verification
• Uses rules for inference and mathematical
reasoning, including mathematical
induction
• Difficult, perhaps impossible to automate
the process
3
Proving Program Correctness
• Two major steps:
– Prove partial correctness: that is, prove that the
program produces correct output if it terminates
– Prove that the program always terminates
• Two propositions involved:
– initial assertion: gives properties input values
must have
– final assertion: gives properties output should
have, if program performed correctly
4
Proving Program Correctness
• A program or program segment S is said to
be partially correct with respect to initial
assertion p and final assertion q if:
– whenever p is true for the input values of S and
S terminates,
– q is true for output values of S
• The notation p{S}q indicates such partial
correctness
5
Partial Correctness
• Note that partial correctness does not state
that a program always terminates; it focuses
on whether or not a program performs
correctly if it terminates
• Note also that partial correctness is only
proven within the context of the initial and
final assertions
6
Example 1
• Show that the following program segment is
correct with respect to the assertions below:
– program segment:
y = 2;
z = x + y;
– initial & final assertions:
p: x = 1
q: z = 3
7
Example 1
• Suppose p is true: x equals 1 when program
begins
• Than y is assigned 2, and z is assigned the
sum of x and y, or 3
• Since z=3 is the final assertion, p{S}q is
true
8
Rules of Inference and Program
Correctness
• Several rules of inference are useful in
proving program correctness
• The first of these is called the composition
rule, which in essence states that a program
is correct if each of its subprograms is
correct
9
Composition Rule
• Suppose a program S is split into subprograms
S1 and S2 - the notation S=S1;S2 indicates S is
made up of S1 followed by S2
• Suppose S1 and S2 can each be proven partially
correct with respect to assertions p, q and r - then
we have p{S1}q and q{S2}r
• Thus, if p is true and S=S1;S2 executes and
terminates, then r is true
10
Composition Rule
• Stated mathematically, the composition rule
is:
p{S1}q
q{S2}r
-------------- p{S1;S2}r
11
Conditional Statements
• Conditional statements are program
segments of the form: if condition then S
(where S is a block of statements)
– When condition is true, S is executed
– When condition is untrue, S is not executed
12
Conditional Statements
• To verify the segment is correct with respect
to initial assertion p and final assertion q:
– show that when p is true and condition is true,
then q is true after S terminates
– show that when p is true and condition is false,
then q is true (that is, S does not execute)
13
Rule of Inference for Conditional
Statements
(p  condition){S}q
(p  condition)  q
------------------------------------ p{if condition then S}q
14
Example 2
• Verify that the following program segment
is correct with respect to initial assertion
p=T and final assertion q = y  x:
if x > y then y := x
• Since p=T, we need only check condition:
– if x > y is true, y := x; thus y  x, so q is true
– if x > y is not true, then y  x, so q is true
• The program is correct with respect to given
p and q
15
More complex conditional
statements
• With a statement of the form:
if condition then S1 else S2
the logic is somewhat more complicated: if
condition is true, S1 executes; if condition is
untrue, S2 executes
16
Verifying more complex
conditionals
• To verify segment correct with respect to
initial assertion p and final assertion q:
– show that when p is true and condition is true, q
is true after S1 terminates;
– show that when p is true and condition is false,
q is true after S2 terminates
17
Rule of Inference
(p  condition){S1}q
(p  condition){S2}q
--------------------------------------------- p{if condition then S1 else S2}q
18
Example 3
Verify that the program segment:
x:=2
z:=x+y
if y > 0 then
z:=z+1
else
z:=0
is correct with respect to initial assertion y=3
and final assertion z=6
19
Example 3
• Start by assuming p is true: that is, y=3
• The assignment statements preceding the
conditional set x to 2 and z to the sum of x
and y, or 5
• Since y=3 and 3>0, the condition is true,
and the assignment statement sets z to z+1,
or 6
• So at the end, z=6 and q is true
20
Loops and loop invariants
• A loop is a statement of the form:
– while condition S
– where S is executed repeatedly until condition
becomes false
• A loop invariant is an assertion that remains
true each time S is executed
• Assertion p is a loop invariant if
(pcondition){S}p is true
21
Rule of Inference for Loops
(p  condition){S}p
--------------------------------------------- p{while condition S}(condition  p)
22
Example 4
• Verify the program segment below
terminates with factorial = n! when n  Z:
x := 1
factorial := 1
while x < n
x=x+1
factorial = factorial * x
– Let p be the proposition: factorial:=x! and x<=n
– We need to prove [p  (x < n)]{S}p in order to
prove p{while x<n S}[(x  n)  p] is true
23
Example 4
• Note that p is true before the loop is entered,
since at that that point factorial=1=1!
• Assume p is true and x<n after one iteration of
the loop
– assume loop executes again: x increments by 1
– x is still <= n, since by the inductive hypothesis x<n
before loop is entered, and x & n are positive
– factorial, which was (x-1)! by the inductive
hypothesis, is set to (x-1)!*x = x!
24
Example 4
• So p remains true, and p is a loop invariant
– then [p  (x < n)]{S}p is true
– if follows that p{while x<n S}[(x  n)  p] is true
• The loop terminates after n-1 iterations with
x=n, since x was 1 at the beginning of the
program, is incremented by 1 during each
iteration, and the loop terminates when x  n
• So, at termination, factorial = n!
25
Proving correctness of entire
programs
• Split the program into segments: the rule of
composition can be used to build the
correctness proof
• Prove the correctness of each segment: for
example, if there are 4 segments, prove
p{S1}q, q{S2}r, r{S3}s, and s{S4}t
• If all are true, then p{S}t is true
• If all 4 segments terminate, then S
terminates, and correctness is proven
26
Section 3.6
Program Correctness
- ends -
27