Transcript Chapter 18d - McGraw Hill Higher Education

Programming Languages
2nd edition
Tucker and Noonan
Chapter 18
Program Correctness
To treat programming scientifically, it must be possible to specify the
required properties of programs precisely. Formality is certainly
not an end in itself. The importance of formal specifications must
ultimately rest in their utility - in whether or not they are used to
improve the quality of software or to reduce the cost of
producing and maintaining software.
J. Horning
Copyright © 2006 The McGraw-Hill Companies, Inc.
Contents
18.1 Axiomatic Semantics
18.2 Formal Methods Tools: JML
18.3 Correctness of Object-Oriented Programs
18.4 Correctness of Functional Programs
18.4.1 Recursion and Induction
18.4.2 Examples of Structural Induction
Copyright © 2006 The McGraw-Hill Companies, Inc.
18.4 Correctness of Functional Programs
Pure functional programs are more accessible to
correctness proofs than imperative or OO programs.
Three major reasons:
1. Pure functional programs are state-free (no assignment),
2. Functions and variables mathematical ideas, and
3. Recursion aligns well with proof by induction.
Copyright © 2006 The McGraw-Hill Companies, Inc.
18.4.1 Recursion and Induction
Consider the Haskell function:
> fact n
> | n == 1
> |n>1
=1
= n*fact(n-1)
-- fact.1
-- fact.2
Suppose we want to prove that this function correctly computes
the factorial. I.e., that it computes:
fact(1) = 1
fact(n) = 12…(n-1)n
when n>1
Copyright © 2006 The McGraw-Hill Companies, Inc.
Induction proof of a recursive function
The induction proof is straightforward. We use the definition
of the function directly in the proof.
Basis step: The function computes the correct result for n = 1,
using line fact.1 of the definition.
Induction step: Assume the hypothesis that the function
computes the correct result for some n = k > 1. That is, it
computes fact(k) = 12…(k-1)k. Then for n = k+1, it
computes fact(k+1) = (k+1)*fact(k) using line fact.2 of the
definition. Thus, it computes fact(k+1) = 12…(k1)k(k+1), which completes the induction step.
Copyright © 2006 The McGraw-Hill Companies, Inc.
18.4.2 Examples of Structural Induction
List concatenation and reversal:
> cat [] ys
= ys
-- cat.1
> cat (x:xs) ys
= x : (cat xs ys)
-- cat.2
> rev []
= []
-- rev.1
> rev (x:xs)
= cat (rev (xs)) [x] -- rev.2
Suppose we want to prove the following property about the
relationship between cat and rev:
rev (cat xs ys) = cat (rev ys) (rev xs)
E.g.,
rev (cat “hello ” “world”) = cat (rev “world”) (rev “hello ”)
= “dlrow olleh”
Copyright © 2006 The McGraw-Hill Companies, Inc.
The Proof
Basis step:
from cat.1
= cat (rev ys [])
from rev.2
= cat (rev ys rev [] from rev.1
Induction step:
Hypothesis: rev (cat xs ys) = cat (rev ys) (rev xs)
rev (cat (x:xs) ys) = rev x : (cat xs ys)
from cat.2
= rev (cat (xs ys) [x])
from rev.2
= cat (cat (rev ys) (rev xs)) [x] from hypothesis
= cat (cat (rev ys) (rev xs)) [x] cat associativity*
= cat (rev ys) (rev (x:xs))
from rev.2
*Note: associativity of cat needs to be proved separately.
rev (cat [] ys) = rev (ys)
Copyright © 2006 The McGraw-Hill Companies, Inc.
List Length and Concatenation
> len []
=0
-- len.1
> len (x:xs) = 1 + (len xs)
-- len.2
E.g.,
len [1,3,4,7] = 1 + len [3,4,7]
= 1 + (1 + len [4,7])
= 1 + (1 + (1 + len [7]))
= 1 + (1 + (1 + (1 + len [])))
= 1 + (1 + (1 + (1 + 0)))
=4
Suppose we want to prove the following property about the
relationship between len and cat:
len (cat xs ys) = len xs + len ys
Copyright © 2006 The McGraw-Hill Companies, Inc.
The Proof
Basis step:
len (cat [] ys) = len (ys)
= 0 + len (ys)
= len [] + len ys
from cat.1
from arithmetic
from len.1
Induction step:
Hypothesis: len (cat xs ys) = len xs + len ys
len (cat (x:xs) ys) = len x : (cat xs ys)
= 1 + len (cat xs ys)
= 1 + len xs + len ys
= len x:xs + len ys
Copyright © 2006 The McGraw-Hill Companies, Inc.
from cat.2
from len.2
from hypothesis
from len.2