← Back to System Internals

The Procedure Call

How Gries brings the named procedure into the calculus: a procedure is a command with a specification, a call is checked against that specification alone, and parameter passing is nothing more than disciplined substitution — provided you never let the actuals alias.

Up to this point Gries’ language has been a handful of primitive commands whose weakest preconditions you compute directly. The procedure adds the one thing every real program depends on: abstraction. A procedure packages a command behind a name and a specification, so that a caller can use it without reading its body. The whole payoff — and the whole discipline — is that you reason about a call using only the procedure’s pre/postcondition, treating the body as a sealed box. This page works through what a procedure specification is, how the three parameter modes reduce to substitution, the proof rule for a call, the aliasing restriction that keeps the substitution honest, and how recursion is proved with the same bound-function idea that terminates a loop.

Procedures and abstraction

A procedure is a named command equipped with a specification — a precondition pre and a postcondition post. The declaration ties the name to a body, but the body is deliberately hidden from anyone who calls it. What the caller sees is the contract:

proc P(value x; result y):
    # pre:  pre(x)
    # post: post(x, y)
    body       # hidden from the caller

This is the essence of modularity. The author of P proves once that the body meets the specification — {pre(x)} body {post(x,y)} — and from then on every caller reasons from the spec, never from the body. A hundred call sites do not require a hundred re-readings of the implementation; each is checked against two predicates. Change the body later, keep the spec, and every caller stays correct without being touched. Abstraction is precisely this decoupling of “what is guaranteed” from “how it is achieved.”

Read that as a two-sided bargain. The caller owes the precondition; the procedure owes the postcondition. Neither side needs to know how the other keeps its half. That is what makes proofs compositional: the correctness of a large program is assembled from the specifications of its parts, not from their internals.

Parameters and passing modes

Parameters connect the fixed names inside a procedure to the varying data at a call site. Two vocabularies must never be confused:

• Formal parameters — the names in the declaration (x, y above). They are local placeholders; the spec is written in terms of them.
• Actual parameters — the expressions or variables supplied at a call (P(a, z)). They are what the formals stand for during that particular call.

Gries treats three passing modes, and the point of each is how it maps to substitution when you reason about a call.

The critical thing Gries insists on is that these are copy semantics, not reference (pointer/aliasing) semantics. Because a value comes in as a copy and a result goes out as a copy, the effect of a call can be described purely by textual substitution of actuals for formals — the same backward-substitution machinery used for assignment. That is the whole reason the proof rule below is so clean, and also the whole reason aliasing (Section 4) is forbidden: aliasing is exactly what breaks the copy model.

The proof rule for a call

Take a procedure with a value parameter and a result parameter:

proc P(value x; result y):   # {pre(x)} body {post(x, y)}

To reason about the call P(a, z) — passing expression a for the value formal x, and variable z for the result formal y — you substitute the actuals for the formals throughout the specification. The obligation splits into two halves, matching the bargain of Section 1:

In weakest-precondition form, a call must guarantee the caller’s postcondition R no matter what result the procedure legitimately produces. So wp requires the precondition to hold now, and that every result value permitted by post would establish R once written back into z:

The universal quantifier is doing real work: it says whatever value the (possibly nondeterministic) procedure returns, as long as it is one post allows, the caller’s goal R must follow. If the procedure is deterministic and post(a, res) pins res to a single value, the quantifier collapses to a plain substitution — you just plug that value in for z. A worked call:

proc Double(value x; result y):
    # pre:  x ≥ 0
    # post: y = 2*x

# Caller wants:  R = (z > 6)   after   Double(n, z)

# wp("Double(n, z)", z > 6)
#   = pre(n) ∧ (∀ res : post(n,res) ⇒ (z>6)[z:=res])
#   = (n ≥ 0) ∧ (∀ res : res = 2*n ⇒ res > 6)
#   = (n ≥ 0) ∧ (2*n > 6)
#   = (n ≥ 0) ∧ (n > 3)
#   = n > 3

# So {n > 3} Double(n, z) {z > 6}   — proven without opening the body.

Notice that the body of Double never appeared. The call was discharged entirely from pre, post, and substitution — which is exactly the modularity claim of Section 1 made mechanical.

Aliasing — the classic pitfall

The substitution rule is sound only if each actual names a distinct piece of state. Aliasing — when two names refer to the same variable — silently invalidates the copy model, because a “copy out” to one name is unexpectedly visible through the other. Two aliasing situations bite:

• The same variable is passed to two parameters (especially two result or value-result parameters).
• A variable is passed as a parameter and also referenced inside the procedure as a global.

Consider a swap procedure specified to exchange its two value-result arguments. The spec is proven for distinct actuals; alias them and the guarantee evaporates:

proc Swap(value-result u, v):
    # post: u = V0 and v = U0   (U0,V0 = entry values)
    t := u ;  u := v ;  v := t

# Aliased call: pass the SAME variable twice
# Swap(a, a)

# Spec, naively substituted u,v := a,a, claims:
#   post: a = A0 and a = A0     (looks fine!)
# But copy-in gives u=A0, v=A0; the body swaps
# copies, then BOTH copy-outs write back to a.
# Result depends on copy-out order — surprise, and
# the two formals were never independent. Unsound.

proc Swap(value-result u, v):
    # post: u = V0 and v = U0
    t := u ;  u := v ;  v := t

# Distinct call: two different variables
# Swap(a, b)

# Substituting u,v := a,b in post:
#   a = B0 and b = A0
# copy-in: u=A0, v=B0; body swaps copies;
# copy-out: a := (new u)=B0, b := (new v)=A0.
# Exactly the postcondition. Sound. ✓

Gries’ response is a blunt restriction rather than a repair: the actual parameters of a call must not alias one another, and must not alias any global the procedure accesses. Under that restriction the substitution rule of Section 3 is sound; violate it and the proof rule simply does not apply, so no guarantee is inherited from the specification. It is the caller’s obligation to supply non-aliasing actuals — a proof obligation, not a runtime hope.

Recursive procedures

A recursive procedure calls itself, so its correctness proof appears circular: to prove the body correct you must already know that the recursive call is correct. Gries breaks the circle with induction, and rules out infinite regress with a bound function — exactly the device that terminates a loop.

• Inductive hypothesis. When proving the body, you are allowed to assume the procedure’s specification already holds for the recursive call — but only for arguments that are “smaller.” You reason as if the call on the smaller problem is a proven primitive.
• Bound / variant. To make “smaller” precise and guarantee termination, choose an integer expression t over the parameters that is ≥ 0 whenever the precondition holds and strictly decreases before every recursive call. An integer cannot decrease forever while staying non-negative, so the recursion bottoms out in finitely many calls.

This is the same well-ordering argument used for the loop: the bound function of a loop and the variant of a recursion are the identical idea — a value counting down to a guaranteed stop. (See bound functions for the general treatment.) A worked example on factorial:

proc Fact(value n; result f):
    # pre:  n ≥ 0
    # post: f = n!
    # bound (variant) t: n         # ≥ 0 and drops by 1 per call
    if n = 0 → f := 1
    [] n > 0 →
         Fact(n - 1, g) ;   # recursive call on smaller n
         f := n * g
    fi

# TERMINATION (variant t = n):
#   pre gives n ≥ 0, so t ≥ 0.
#   recursive call uses n-1 < n, so t strictly
#   decreases → finitely many calls. ✓

# CORRECTNESS (induction on n):
#   base  n = 0: f := 1 = 0!            ✓ post
#   step  n > 0: assume spec holds for n-1,
#         so after Fact(n-1, g): g = (n-1)!
#         then f := n*g = n*(n-1)! = n!  ✓ post

# Note: actuals (n-1) and g are distinct — no
# aliasing, so the call rule of §3 applies.

The inductive hypothesis (“assume the spec for n-1”) is legitimate precisely because the variant guarantees the assumed-about case is strictly smaller; the induction is well-founded. A recursion with no decreasing bound is the analogue of a loop with no bound function — possibly non-terminating, and therefore unproven.

Procedures vs inlining

One could always inline a procedure — textually paste its body at every call site and reason about the expanded program. It would even be sound. But it discards the one property that makes large proofs feasible: compositionality. Reasoning through the spec, as in Section 3, keeps each call’s proof local and bounded by two predicates; inlining forces you to re-read and re-prove the body at every site, and re-do all of it whenever the body changes.

The governing principle: a body may be replaced freely as long as it still meets the specification. Any two bodies satisfying the same {pre} body {post} are interchangeable to every caller — that substitutability is abstraction, and it is the reason to prefer spec-based reasoning over inlining even though both are sound. The specification, not the code, is the interface.

Summary