Recitation 17: Verification Example, Review of Logic

In the previous lecture, we saw an example of verification. Today we'll look at another example.

Consider the following recursive implementation of a function lmax that computes the maximum element of a nonempty list:

(* Returns: lmax xs  is the maximum element in the list xs.
 * Checks: xs != []
 *)
let rec lmax (xs : int list) : int =
    match xs with
        [] -> raise (Failure "requires clause of max violated")
      | [x] -> x
      | x :: t -> max x (lmax t)

How do we handle recursive functions? We'll use the approach of assuming that a recursive function satisfies its spec whenever it is called recursively. A proof of correctness will then ensure the partial correctness of the function's implementation, which we can distinguish from total correctness:

Partial correctness: whenever the function is applied with the precondition satisfied, and it terminates, it produces results satisfying the postcondition.
Total correctness: the function has partial correctness, and in addition, it always terminates when the function is applied.

The nice thing about this approach is that we can separate the problem of proving that a function computes the right answer from the problem of proving that the function terminates.

Partial Correctness

Let's prove partial correctness. First of all, we need to understand our postcondition a little more precisely. What are the elements of a list? We can define a function that gives us the elements by induction on the list:

elements([]) = ∅
elements(h :: t) = {h} ∪ elements(t)

Like an abstraction function, this function maps from the concrete domain of OCaml lists to a more abstract mathematical domain, that of sets.

Expression Assumptions Justification

lmax xs xs ≠ [] Consider an arbitrary call satisfying the precondition.

match xs with []-> ... xs ≠ [] Expand the function body. Now we need to create cases to know which way the match will go. Here are three exhaustive cases: xs = [], xs = [x], xs = x :: t.

Case xs = []

raise (Failure ...) xs ≠ [] This case can't happen according to our assumptions. The postcondition is vacuously satisfied.

Case xs = [x] = x :: []

x xs = [x] The result is the only element in xs, so elements(xs) = {x}, and therefore x is the maximum element in elements(xs).

Case xs = x::t and t ≠ []

max x (lmax t) xs = x::t
t ≠ [] Now lmax can be applied to t; crucially, t is not the empty list, so the precondition of lmax is satisfied.

max x n1 xs = x::t
t ≠ []
n1 = maximum of elements(t) Now we can apply the function max, using its spec, obtaining some value n2 that satisfies the postcondition of max.

n2 xs = x::t
t ≠ []
n1 = maximum of elements(t)
(n2 = x or
n2 = n1)
n2 ≥ x
n2 ≥ n1 From the mathematical definition of the maximum element of a set, the value n1 must be an element of t and must be at least as large as any element of t. The specification says that n2 must be an element of xs and at least as large as any element of xs. We know from the definition of elements that elements(xs) = {x}∪elements(t). So n2 must be an element of xs because it's either x or it's n1, which is an element of t. Further, n2 must be at least as large as x (n2 ≥ x). And it must be at least as large as elements(t), since it's at least as large as n1, which is at least as large as any element of t. Therefore n2 is the maximum element of xs in this case.

QED

Expression	Assumptions	Justification
`lmax xs`	xs ≠ []	Consider an arbitrary call satisfying the precondition.
`match xs with []-> ...`	xs ≠ []	Expand the function body. Now we need to create cases to know which way the `match` will go. Here are three exhaustive cases: xs = [], xs = [x], xs = x :: t.
Case xs = []
`raise (Failure ...)`	xs ≠ []	This case can't happen according to our assumptions. The postcondition is vacuously satisfied.
Case xs = [x] = x :: []
`x`	xs = [x]	The result is the only element in `xs`, so elements(xs) = {x}, and therefore x is the maximum element in elements(xs).
Case xs = x::t and t ≠ []
`max x (lmax t)`	xs = x::t t ≠ []	Now `lmax` can be applied to t; crucially, t is not the empty list, so the precondition of `lmax` is satisfied.
`max x n1`	xs = x::t t ≠ [] n1 = maximum of elements(t)	Now we can apply the function `max`, using its spec, obtaining some value n2 that satisfies the postcondition of `max`.
`n2`	xs = x::t t ≠ [] n1 = maximum of elements(t) (n2 = x or n2 = n1) n2 ≥ x n2 ≥ n1	From the mathematical definition of the maximum element of a set, the value n1 must be an element of t and must be at least as large as any element of t. The specification says that n2 must be an element of xs and at least as large as any element of xs. We know from the definition of elements that elements(xs) = {x}∪elements(t). So n2 must be an element of xs because it's either x or it's n1, which is an element of t. Further, n2 must be at least as large as x (n2 ≥ x). And it must be at least as large as elements(t), since it's at least as large as n1, which is at least as large as any element of t. Therefore n2 is the maximum element of xs in this case.
QED

Total Correctness

The key to proving total correctness is to prove that recursion cannot go on forever. We need to be able to map the function arguments onto a set that has a least element. Typically we do this by giving a decrementing function d(x) that maps the function argument x onto the natural numbers. The decrementing function d has two properties:

It maps any function arguments that satisfy the precondition to a natural number (≥ 0):
PRE ⇒ 0 ≤ d(x)
Whenever there is a recursive call, the decrementing function applied to the arguments x' of the recursive call is strictly smaller:
0 ≤ d(x') < d(x).

This means that when the decrementing function is zero, there is no recursive call.

These conditions ensure that the decrementing function keeps getting smaller on every recursive call, but cannot get smaller forever.

For example, in lmax an appropriate decrementing function is: d(x) = List.length(x) − 1. It must be nonnegative; when it is zero, the function terminates; and the recursive call to lmax is on a shorter list t.

A review of propositional logic

Recall from CS 2800 that propositional logic is a logic built up from simple symbols representing propositions about some world. For our example, we will use the letters A, B, C, ... as propositional symbols. For example, these symbols might stand for various propositions:

A = "got 90% on the final"
B = "attended class every time"
C = "got an A in the class"
D = "x + 1 ≤ y"
E = "e ∈ s"

It is not the job of propositional logic to assign meanings to these symbols. However, we use statements to the meanings of D and E to talk about the correctness of programs.

We define a grammar for propositions built up from these symbols. We use the letters P, Q, R to represent propositions (or formulas):

P,Q,R ::= ⊤              (* true *)
        | ⊥              (* false *)
        | A, B, C        (* propositional symbols *)
        | ¬P             (* sugar for P⇒⊥ *)
        | P ∧ Q          (* "P and Q" (conjunction) *)
        | P ∨ Q          (* "P or Q" (disjunction) *)
        | P ⇒ Q         (* "P implies Q" (implication) *)
        | P ⇔ Q         (* "P if and only if Q" (double implication) *)

Note: On some browsers, on some operating systems, in some fonts, the symbol for conjunction (and) is rendered incorrectly as a small circle. It should look like an upside-down ∨. In these course notes, it will appear variously as ∧, ∧, or ∧.

The precedence of these forms decreases as we go down the list, so P ∧ Q ⇒ R is the same as (P ∧ Q) ⇒ R. One thing to watch out for is that ⇒ is right-associative (like →), so P ⇒ Q ⇒ R is the same as P ⇒ (Q ⇒ R). We will introduce parentheses as needed for clarity. We will use the notation for logical negation, but it is really just syntactic sugar for the implication P ⇒ ⊥. We also write P ⇔ Q as syntactic sugar for (P ⇒ Q) ∧ (Q ⇒ P), meaning that P and Q are logically equivalent.

This grammar defines the language of propositions. With suitable propositional symbols, we can express various interesting statements, for example:

A ∧ B ⇒ C: "If I got a 90% on the final and I attended class, I will get an A"
¬C ⇒ (¬A ∨ ¬B): "If I didn't get an A in the class, then either I didn't get a 90% on the final or I didn't attend class"
C ∨ ¬A ∨ ¬B: "Either I got an A in the class, or I didn't get a 90% on the final or I didn't attend class"

In fact, all three of these propositions are logically equivalent, which we can determine without knowing about what finals and attendance mean.