← CatZep/Engineering Guides/The Science of Programming

Predicates, States & Quantification

The logic prelude of Gries’ The Science of Programming — what a predicate really is, how to quantify over ranges, and the textual-substitution machinery that turns a postcondition into a precondition.

Before you can prove a single program correct you have to be fluent in the language you reason in. In The Science of Programming, David Gries spends the opening chapters on exactly that: the predicate calculus. A specification is nothing more than two predicates — a precondition and a postcondition — and a proof is a chain of implications between predicates. If your predicate algebra is shaky, program proofs are impossible. This page distils the pieces that matter most for the programming that follows: predicates as sets of states, quantification with Gries’ linear notation, textual substitution, and the altered-function notation for reasoning about arrays.

Concepts explained in this guide

Read these definitions first, or use the linked terms as you go. The examples and limitations are local to this guide; companion pages are optional.

Predicates as sets of states

A state is an assignment of values to the program’s variables — one point in the space of everything the variables could be. A predicate is a boolean expression over those variables; equivalently, and this is the shift in view that unlocks everything, a predicate names the set of states in which it is true.

Under the set reading, the logical connectives become set operations: ∧ is intersection, ∨ is union, ¬ is complement. And implication becomes containment: P ⇒ Q exactly when the set of P-states is a subset of the set of Q-states. That is why a stronger predicate (fewer states, more restrictive) implies a weaker one — F is the strongest predicate of all, T the weakest.

Every assertion you sprinkle through a program — a precondition, a postcondition, a loop invariant — is one of these predicates, carving out the set of states the program is allowed to be in at that point. Nothing more exotic is going on.

The predicate calculus

The predicate calculus extends ordinary propositional logic (the algebra of ∧, ∨, ¬, ⇒, ≡) with predicates over variables and quantifiers that bind those variables. Two notions become central the moment quantifiers appear.

• Free variable. A variable occurrence not governed by any quantifier. In x > 0 ∧ (∀ i : 0 ≤ i < n : b[i] > 0), the occurrences of x, n, and b are free — they refer to the surrounding program state.
• Bound variable. A variable introduced and controlled by a quantifier, like i above. It is a local placeholder; its name is irrelevant and can be changed at will (i to j) without altering meaning.

Substitution notation

R[x := e] denotes the predicate R with every free occurrence of x replaced by the expression e. Bound occurrences are left untouched. This single operation is, quite literally, the engine of the assignment axiom later on.

A worked example. Let R be x < y ∧ x ≥ 0. Then:

# R           :  x < y  and  x ≥ 0
# R[x := x+1] :  (x+1) < y  and  (x+1) ≥ 0
#             =  x < y-1  and  x ≥ -1

# only the free x's changed; y was untouched

Two hazards Gries insists on

Substitution looks purely mechanical, but two things can silently corrupt it.

# R:  (∃ y : y > x)      "some y exceeds x"

# Naively compute R[x := y]:
#   (∃ y : y > y)   ← FALSE, always

# The free x was CAPTURED by the
# bound y. Meaning changed entirely.

# Rename bound y to a fresh k:
#   R:  (∃ k : k > x)

# Now substitute safely:
#   R[x := y] = (∃ k : k > y)   ✓

# Same meaning, no capture.

The rule: if e mentions a variable that is bound inside R, rename that bound variable to something fresh before substituting. Otherwise the substitution “captures” a free variable of e and changes the predicate’s meaning.

The second hazard is definedness. Substitution is only meaningful when e is actually defined in the states you care about — no division by zero, no array index out of bounds. Gries carries a domain condition alongside a substitution: R[x := e] is only trustworthy where domain(e) holds (e.g. b[i] requires 0 ≤ i < n). This resurfaces as the definedness proviso in the assignment axiom.

Quantification

Gries uses a clean linear notation with three explicit parts — a bound variable, a range, and a term — which avoids the ambiguity of the classic ∀ i . … form.

• Bound variable i — the local placeholder the quantifier introduces.
• Range R — a predicate on i that restricts which values are considered, e.g. 0 ≤ i < n. Only values satisfying the range contribute.
• Term P — the predicate (or, for ∑/∏ forms, the expression) evaluated for each in-range i.

Read (∀ i : R : P) as “for every i such that R, we have P” and (∃ i : R : P) as “for some i such that R, we have P.” The same skeleton generalises to sum (∑ i : R : t) and product (∏ i : R : t), where the term is a numeric expression rather than a predicate.

The empty-range rules

What is the value of a quantification whose range admits no i? These conventions are not arbitrary — they are the identity elements that make range-splitting work, and they matter constantly at loop initialisation (an empty prefix).

Laws for manipulating quantifiers

These identities are the workhorses of every array proof. You will reach for range-splitting and the one-point rule in nearly every loop invariant.

The range-split law is the one that makes loops tick. Extending (∀ i : 0 ≤ i < k : P) to k+1 is just splitting off the singleton i = k, then collapsing it with the one-point rule to P[i := k] — exactly the extra fact one loop iteration must establish.

State manipulation & arrays

Arrays force one more idea. An array b is best treated as a function from indices to values: b[i] is function application. So what does the assignment b[i] := e do to a predicate? It cannot just textually replace b[i] — other subscripts like b[j] might refer to the same element when j = i, and naive replacement would miss that aliasing.

Gries’ answer is the altered-function notation. Write (b; i:e) for “the array b everywhere the same, except that index i now maps to e.” Formally it is the function:

With this, the assignment b[i] := e is treated exactly like an ordinary assignment to the whole array variable b: it replaces b by (b; i:e). Substitution into a predicate then handles all the aliasing correctly, because evaluating (b; i:e)[j] forces you to compare j with i.

# post R:  b[j] = 5
# command:  b[i] := 7

# Naive: "b[i] does not appear in R,
# so R is unchanged" → precond b[j]=5

# WRONG when i = j: after b[i]:=7
# b[j] is 7, not 5. Aliasing ignored.

# Replace b by (b; i:7) throughout R:
#   R[b := (b; i:7)]  =  (b; i:7)[j] = 5

# Expand the application by cases:
#   if j = i :  7 = 5   → F
#   if j ≠ i :  b[j] = 5

# precond:  j ≠ i  and  b[j] = 5   ✓

This is not a curiosity — it is exactly the reasoning you need for any program that mutates an array, and every array-loop derivation in the book leans on it.

Textual substitution is the engine

Everything above converges on one payoff. The assignment axiom — the rule that gives the weakest precondition of an assignment — is pure textual substitution. There is no separate theory of assignment; there is only the substitution you just learned.

Read it plainly: to find what must hold before an assignment so that R holds after, take R and substitute backward. Scalar assignment substitutes the expression for the variable; array assignment substitutes the altered function for the array. The capture and definedness cautions from the substitution section are precisely why the axiom carries a domain(e) conjunct and why bound variables must be renamed. Master substitution here and the command semantics come almost for free — the full treatment of the commands and their weakest preconditions is in the commands and their wp.

Common quantified assertions in programs

A handful of quantified predicates recur so often in loop invariants that they are worth memorising as idioms. Each says something precise about a prefix or a slice of an array b. These are exactly the building blocks of the invariants in developing loops from invariants.

Notice how “x not in b[0..i-1]” is the De Morgan dual of an existential, and how “sorted” ranges over adjacent pairs so the singleton and empty prefixes are trivially sorted (empty range ⇒ T). When a loop advances i to i+1, you extend each of these by range-splitting off the new index and discharging the one extra fact — the whole reason the quantifier laws earned their place above.

Worked example: an empty universal and a bounded array claim

Work through the state changes and the exact claim being checked.

Run and change the example

Download guide_labs.py. Python 3.10+, standard library only. In its directory, run:

python3 guide_labs.py quantifiers
python3 guide_labs.py test

The complete standard-library lab checks the stated finite cases and boundary inputs. Its invariants explain the reasoning; tests alone do not prove all possible inputs.

The program tests its stated finite contracts. It is an educational model, not an implementation of the named production product or a proof of unmodeled distributed faults.

Summary