Capstone: proving programs correct and an introduction to graphs

This final lesson applies the whole course to two topics at the heart of computing science. The first is program correctness: using preconditions, postconditions and loop invariants to prove that code does what it should for every input, not just the inputs you tested. The second is graphs: the discrete structure that models networks, dependencies, maps and relationships of every kind. Both lead directly into CMPUT-204 (Algorithms I), where you will prove algorithms correct and analyze their running time.

Specifications: preconditions and postconditions

To prove a program correct we must first say precisely what correct means. A specification gives a precondition, a predicate that must hold before the code runs, and a postcondition, a predicate that must hold after it finishes. The program is correct with respect to the specification if, whenever it starts in a state satisfying the precondition, it terminates in a state satisfying the postcondition. This is written as a Hoare triple, named after the British computer scientist Tony Hoare.

For example, \(\{x = 5\}\; x := x + 1\; \{x = 6\}\) is a valid triple. So is \(\{x > 0\}\; x := 2x\; \{x > 0\}\). The triple \(\{\text{true}\}\; y := x \cdot x\; \{y \ge 0\}\) is valid over the integers, since squares are never negative. Observe how the predicate logic of lesson 4 supplies the language for P and Q. The triple form proves partial correctness: correct if the program stops. Total correctness adds a proof of termination.

The table shows how earlier lessons reappear. The rule for if statements is proof by cases from lesson 6. The rule for sequences is the transitivity of implication. The rule for loops, which we look at next, is induction from lesson 10.

Loop invariants

A loop invariant is a predicate about the program's variables that is true before the loop starts and remains true after every iteration. Proving a loop correct with an invariant has three parts, and they line up exactly with an induction proof on the number of iterations.

Choosing the invariant is the creative step. A good invariant usually describes the work done so far: the part of the list already summed, already searched or already sorted. It is often a weakened form of the postcondition, with the final value replaced by the loop variable: the postcondition says the sum of all n elements, and the invariant says the sum of the first i.

def sum_list(xs):
    total, i = 0, 0
    assert total == sum(xs[:i])                    # invariant: initialization
    while i < len(xs):
        total += xs[i]
        i += 1
        assert total == sum(xs[:i]) and 0 <= i <= len(xs)   # invariant: maintenance
    assert i == len(xs) and total == sum(xs)       # termination gives the postcondition
    return total

import random
random.seed(272)
for _ in range(1000):
    xs = [random.randint(-50, 50) for _ in range(random.randint(0, 20))]
    sum_list(xs)
print("invariant assertions held on 1000 random lists")

invariant assertions held on 1000 random lists

Writing invariants as assert statements, as above, is a valuable habit even when you do not write a full proof. The assertions document why the code works, and if a later change breaks the reasoning, a test run fails at the exact line where the invariant stopped holding. Production code often disables assertions for speed, but they remain useful during development and testing.

A harder example: binary search

Binary search, which you met in CMPUT-174, is famously easy to get almost right. Jon Bentley reported that most professional programmers he asked could not write a correct version, and a bug in the Java standard library's binary search (an integer overflow in computing the midpoint) went unnoticed for about nine years before it was found in 2006. An invariant makes the reasoning precise.

def binary_search(xs, t):
    lo, hi = 0, len(xs) - 1
    while lo <= hi:
        mid = (lo + hi) // 2
        if xs[mid] == t:
            return mid
        if xs[mid] < t:
            lo = mid + 1
        else:
            hi = mid - 1
    return -1

import random
random.seed(1)
ok = True
for _ in range(2000):
    xs = sorted(random.sample(range(100), random.randint(0, 30)))
    t = random.randint(-5, 105)
    i = binary_search(xs, t)
    ok &= (i == -1 and t not in xs) or (i >= 0 and xs[i] == t)
print("binary search agreed with the specification on 2000 random cases:", ok)

binary search agreed with the specification on 2000 random cases: True

Graphs

A graph \(G = (V, E)\) consists of a set \(V\) of vertices (or nodes) and a set \(E\) of edges, each joining two vertices. In an undirected graph, an edge is an unordered pair \(\{u, v\}\); in a directed graph, an edge is an ordered pair \((u, v)\), drawn as an arrow. A directed graph is exactly a relation on \(V\), the picture used in lesson 9. Graphs model road networks, computer networks, social networks, web links, course prerequisites, state machines and the dependency structure of a software build.

The degree of a vertex in an undirected graph is the number of edges touching it. The first theorem of graph theory, sometimes called the handshaking lemma, relates degrees to edges.

edges = [("A", "B"), ("A", "C"), ("B", "C"), ("B", "D"), ("C", "E"), ("D", "E"), ("E", "F")]
adj = {}
for u, v in edges:
    adj.setdefault(u, set()).add(v)
    adj.setdefault(v, set()).add(u)
deg = {v: len(ns) for v, ns in sorted(adj.items())}
print("degrees:", deg)
print("sum of degrees =", sum(deg.values()), "  2|E| =", 2 * len(edges))
print("odd-degree vertices:", [v for v, d in deg.items() if d % 2])

degrees: {'A': 2, 'B': 3, 'C': 3, 'D': 2, 'E': 3, 'F': 1}
sum of degrees = 14   2|E| = 14
odd-degree vertices: ['B', 'C', 'E', 'F']

Paths, connectivity, trees and Euler paths

A path is a sequence of vertices in which consecutive vertices are joined by edges. A cycle is a path that returns to its start without repeating an edge. A graph is connected if every pair of vertices is joined by some path; connectivity in an undirected graph is an equivalence relation, and its classes are the connected components. Reachability in a directed graph is the transitive closure from lesson 9.

A tree is a connected graph with no cycles. Trees are everywhere in computing: file systems, the parse trees of compilers, the call trees of recursive functions, decision trees and the binary trees of lesson 10. A fundamental theorem says that a tree with \(n\) vertices has exactly \(n - 1\) edges; it can be proved by induction on \(n\), removing a leaf (a vertex of degree 1) in the inductive step.

The oldest problem in graph theory comes from the city of Königsberg, whose seven bridges joined four land areas. Could a walk cross every bridge exactly once? Leonhard Euler proved in 1736 that it could not, founding graph theory. An Euler path uses every edge exactly once. Euler's theorem says a connected graph has an Euler path exactly when it has zero or two vertices of odd degree, and an Euler circuit (returning to the start) exactly when every degree is even. Königsberg's four land areas had odd degrees 3, 3, 3 and 5, so no walk exists.

def euler_status(edges):
    deg = {}
    for u, v in edges:
        deg[u] = deg.get(u, 0) + 1
        deg[v] = deg.get(v, 0) + 1
    odd = [v for v, d in deg.items() if d % 2]
    if not odd:
        return "Euler circuit exists"
    if len(odd) == 2:
        return f"Euler path exists, from {odd[0]} to {odd[1]}"
    return f"no Euler path ({len(odd)} odd vertices)"

konigsberg = [("N", "I"), ("N", "I"), ("S", "I"), ("S", "I"), ("N", "E"), ("S", "E"), ("I", "E")]
print("Konigsberg:", euler_status(konigsberg))
square = [("a", "b"), ("b", "c"), ("c", "d"), ("d", "a")]
print("square:", euler_status(square))
print("square plus diagonal:", euler_status(square + [("a", "c")]))

Konigsberg: no Euler path (4 odd vertices)
square: Euler circuit exists
square plus diagonal: Euler path exists, from a to c

Graph algorithms, including breadth-first and depth-first search, shortest paths, minimum spanning trees and network flow, are a major part of CMPUT-204 and CMPUT-304. Their correctness proofs use the invariants and induction of this lesson, and their analysis uses the counting of lesson 11.

Capstone exercise

The following exercise combines most of the course. A university wants to verify a short program that decides whether a course plan respects prerequisites. Work through each part, using the lesson listed for help.

prereq = {"CMPUT-174": [], "CMPUT-201": ["CMPUT-174"], "CMPUT-272": ["CMPUT-174"],
          "CMPUT-204": ["CMPUT-201", "CMPUT-272"], "CMPUT-304": ["CMPUT-204"]}

def valid_plan(plan):
    assert len(set(plan)) == len(plan)                       # precondition: each course once
    seen = set()
    for k, course in enumerate(plan):
        # invariant: every course in plan[:k] comes after all of its prerequisites
        if any(p not in seen for p in prereq[course]):
            return False
        seen.add(course)
    return True

good = ["CMPUT-174", "CMPUT-272", "CMPUT-201", "CMPUT-204", "CMPUT-304"]
bad = ["CMPUT-174", "CMPUT-204", "CMPUT-201", "CMPUT-272", "CMPUT-304"]
print("good plan valid:", valid_plan(good))
print("bad plan valid: ", valid_plan(bad))
from itertools import permutations
from math import factorial
count = sum(valid_plan(list(p)) for p in permutations(prereq))
print(f"valid orders: {count} of {factorial(len(prereq))}")

good plan valid: True
bad plan valid:  False
valid orders: 2 of 120

Part 6 is a proof by contradiction: suppose a plan is valid and the graph has a cycle \(c_1 \to c_2 \to \cdots \to c_k \to c_1\). Validity forces each course on the cycle to come strictly after the previous one, so \(c_1\) comes after \(c_1\), which is impossible. Writing it out fully is a good test of the habits this course has built: precise definitions, a clear proof method, and complete sentences.

Where to go next

You now have the core vocabulary of theoretical computing science: propositions and predicates, proof techniques, sets, functions, relations, induction, counting and modular arithmetic, invariants and graphs. CMPUT-204 uses all of them to design and analyze algorithms. CMPUT-291 builds databases on relations and predicate logic. CMPUT-331 and CISSP-112 build cryptography on number theory. CMPUT-474 uses sets, functions, countability and diagonal arguments to explore what computers cannot do. Mathematics students can continue with MATH-228 (Introduction to Proofs) and MATH-260 (Discrete Mathematics).