← Back to System Internals

Foundations — Why Correctness, and the Logic of Propositions

The opening move of Gries’ The Science of Programming: why we bother to prove programs correct at all, and the propositional-logic algebra you must own before a single Hoare triple makes sense.

Every serious treatment of program correctness begins not with code but with logic. David Gries’ The Science of Programming (1981) is emphatic about this: you cannot reason precisely about a program until you can reason precisely about the predicates that describe its states. This page covers the two foundational chapters — the motivation (why correctness is worth proving, and what a program really is mathematically) and the propositional calculus that becomes the everyday tool for that reasoning. Get the algebra of ∧, ∨, ¬, ⇒, and ≡ into your fingers here, and the later machinery — predicates with quantifiers in the predicate calculus, and weakest preconditions in the wp calculus — follows almost mechanically.

Why prove programs correct

The case for correctness proofs rests on a single, uncomfortable observation, due to Dijkstra and quoted by Gries: “Testing can show the presence of bugs, but never their absence.” A test exercises one path through one input; passing it tells you nothing about the untried inputs, and for any non-trivial program the untried inputs vastly outnumber the tried ones. A proof, by contrast, argues over all states at once. It attacks the absence of bugs directly, which no finite battery of tests can do.

The economic argument reinforces the logical one. A defect caught while reasoning about a specification costs a moment’s thought; the same defect caught in production — after it has shipped, corrupted data, and woken an on-call engineer — costs orders of magnitude more. The later a bug is found, the more expensive it is to remove, and testing by its nature finds bugs late.

Gries’ thesis, stated in the book’s preface and carried through every chapter, inverts the usual habit:

You do not write the code and then hope to verify it afterward. You start from a specification — a precondition and a postcondition — and let the proof obligations drive each construct you add, so the finished program is correct by construction. Debugging is replaced by derivation.

# write it, run it, patch what breaks
def abs_val(x):
    return x         # "usually positive, ship it"
# is it right for x < 0?  x = 0?
# you find out only when a test fails —
# and only for the inputs you happened
# to try. The rest stay silent bugs.

# state the contract, derive the body
# pre:  T           (any integer x)
# post: r = |x|,  i.e.
#       (r = x or r = -x) and r ≥ 0
# the two guards x ≥ 0 and x ≤ 0
# fall out of the postcondition —
# every case is covered by design.

What a program is, mathematically. To reason this way you need a precise model of what a program means. Gries builds it from two ideas:

• State. A state is an assignment of values to all the program’s variables — a single point in the space of all possible variable combinations. If the variables are x and y, then {x = 3, y = 7} is one state.
• Predicate transformer. A program is a rule that carries states to states. Viewed through the lens of correctness, it is a predicate transformer: given a description of the states you want to end in (the postcondition), it tells you the description of the states you must start in. This backward, predicate-to-predicate view — not the forward, value-to-value one — is what makes derivation possible, and it is developed fully in the wp calculus.

Propositions

A proposition is a boolean expression. Its atoms are the two constants T (true) and F (false) together with boolean variables, combined by five connectives.

Implication is the connective people misread most often. P ⇒ Q is not a claim of cause; it is simply ¬P ∨ Q. In particular it is true whenever P is false — “false implies anything.” Equivalence ≡ (also written ⇔) is boolean equality: P ≡ Q holds when both sides carry the same truth value.

Precedence

To cut parentheses, the connectives bind in this order, tightest first. Use explicit parentheses whenever clarity is at stake.

So ¬P ∧ Q ∨ R ⇒ S parses as ((((¬P) ∧ Q) ∨ R) ⇒ S). When in doubt, over-parenthesise; the algebra below never depends on precedence tricks.

Truth as a set of states

Here is the shift that makes the rest of the book work. Do not think of a proposition (or later, a predicate) as merely “true or false.” Think of it as the set of states in which it is true. Then ∧ is set intersection, ∨ is set union, ¬ is complement, and P ⇒ Q means “the state-set of P is contained in that of Q.” The constant T denotes the set of all states; F denotes the empty set. This picture is what turns implication into subset containment — the backbone of stronger and weaker below.

A small truth table

Every proposition is defined by its truth table — its value in each combination of its variables. Here is P ⇒ Q beside its equivalent ¬P ∨ Q, which is the cleanest way to see that the two are the same proposition.

  P    Q   |  ¬P   |  P ⇒ Q  |  ¬P ∨ Q
-----------+-------+---------+----------
  F    F   |   T   |    T    |    T
  F    T   |   T   |    T    |    T
  T    F   |   F   |    F    |    F
  T    T   |   F   |    T    |    T
# columns for  P ⇒ Q  and  ¬P ∨ Q  match in every row
# therefore  (P ⇒ Q) ≡ (¬P ∨ Q)   is a tautology

A proposition true in every row is a tautology (equivalent to T); one false in every row is a contradiction (equivalent to F). Truth tables are a decision procedure — finite and mechanical — but they blow up as 2n rows for n variables, which is exactly why the algebraic laws in the next section matter: they let you reason without enumerating.

Equivalence transformations

The working method for propositions is not truth tables but rewriting: replace a sub-expression by an equivalent one, over and over, the way you simplify algebra with a(b+c) = ab + ac. Because ≡ is genuine equality of propositions, any law below may be applied to a sub-expression in place, in either direction. The laws are your toolkit for simplifying preconditions, discharging proof obligations, and showing two specifications equal.

A short worked simplification shows the style — each step names the law that licenses it, exactly as you will annotate proof steps later:

# Simplify:  ¬(P ⇒ Q)
  ¬(P ⇒ Q)
≡ ¬(¬P ∨ Q)        # Implication
≡ ¬(¬P) ∧ ¬Q      # De Morgan
≡ P ∧ ¬Q           # Double negation
# So the only way P ⇒ Q fails is  P true and Q false — as expected.

# "not (0 ≤ i and i < n)"
# wrong: people write
#     0 > i and i ≥ n
# — they negated each part but
# kept the AND. That set is empty!
# (i can't be both < 0 and ≥ n)

# ¬(0 ≤ i ∧ i < n)
#   ≡ ¬(0 ≤ i) ∨ ¬(i < n)   (De Morgan)
#   ≡  i < 0  ∨  i ≥ n
# the AND became an OR — the
# out-of-bounds condition, correctly.

The Implication law (P ⇒ Q ≡ ¬P ∨ Q) is worth committing to memory above all others: it lets you eliminate ⇒ entirely and reduce any proof obligation to the four basic connectives, where De Morgan and distribution do the rest.

Natural deduction (briefly)

Equivalence rewriting is one of two styles of formal proof. The other is natural deduction, which works not by substituting equals-for-equals but by applying inference rules that derive new propositions from ones already known. The distinction is worth naming:

• Equivalence rewriting transforms a proposition into an equal one (A ≡ B). It is symmetric and reversible — you can go either direction.
• Inference derives a proposition that follows from premises (A ∴ B, read “therefore”). It is one-directional: from truth of the premises you conclude truth of the consequent, but not vice versa.

The archetypal inference rule is modus ponens: from P and P ⇒ Q, conclude Q.

    P            # premise: P holds
    P ⇒ Q        # premise: P implies Q
  ---------      # modus ponens
    Q            # conclusion: Q holds

A formal proof in this style is a finite sequence of propositions in which every line is either a premise or follows from earlier lines by a named inference rule. Each step is justified — nothing is asserted without a rule that sanctions it. This is precisely the shape a program correctness proof takes: a chain of steps, each licensed by an axiom (assignment, composition) or an inference rule, from the precondition to the postcondition. In practice Gries leans mostly on equivalence rewriting for manipulating predicates, and reserves inference for stitching together the correctness argument at the level of triples — but both are the same underlying discipline of never taking an unjustified step.

Stronger and weaker predicates

Everything the book does later — and the whole point of weakest preconditions — rests on one ordering between propositions, defined purely by implication.

The intuition, once the set picture is in hand, is clean. A stronger predicate makes a bigger claim, so it holds in fewer states — it is more demanding, more restrictive. A weaker predicate asks for less, so it holds in more states — it is more permissive. For example x = 5 is stronger than x > 0 (one state versus infinitely many), and x = 5 ⇒ x > 0.

The two extremes anchor the scale:

• F is the strongest predicate of all — it holds in no state (the empty set), and F ⇒ anything.
• T is the weakest predicate of all — it holds in every state (the full set), and anything ⇒ T.

Now the payoff, which is the reason this page exists. When you ask “what must be true before command S so that R holds afterward?”, there are usually many correct preconditions — and among them, some demand more than necessary. The weakest precondition is the one that demands the least: the most permissive requirement on the starting state that still guarantees the desired result. Anything weaker would let in a state from which S fails to establish R; anything stronger needlessly excludes valid starting states. Choosing the weakest is what makes derivation exact rather than merely sufficient — and that is the operator wp(S, R) introduced in the weakest-precondition calculus. This section is the whole reason “weakest” is the word we want.

Summary