← CatZep/Engineering Guides/The Science of Programming

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.

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.

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

A caller establishes the procedure precondition and relies only on the documented postcondition/frame and termination behavior. The contract can permit several results; every permitted result must establish the caller's required goal.

For a simple value-input/result-output abstraction, evaluate input expression a in the old state as A. Then reason with pre(A) and every res satisfying post(A,res), substituting res for the output variable in the caller goal. Do not re-evaluate a after output changes a variable on which a depends.

# Simple model: frozen input A; only result location z changes.
pre(A) and (for every res:
    post(A, res) implies R[z replaced by res])
# Add nonaliasing/frame conditions required by the procedure model.

More general calls need old-state constants, heap ownership/alias rules, and definedness of actual expressions. The simple formula is not a universal rule for arbitrary reference/global side effects.

Aliasing — the classic pitfall

A formal call rule needs an explicit alias/frame model. Copy-in/copy-out arguments can conflict when two outputs name the same mutable location; reference/object-sharing semantics introduce other effects. Restrictions are model assumptions, not a claim that every aliased call necessarily fails.

A real copy-out counterexample outputs u=1 and v=2, then copies both to a. Final a depends on output order. By contrast, Swap(a,a) with equal input copies yields equal output copies, so it does not demonstrate an order-dependent result.

# Conceptual copy-out counterexample:
# Procedure sets its distinct formal outputs u=1, v=2.
# Call outputs(a,a): copy-out u then v gives a=2;
# copy-out v then u gives a=1.
# Require distinct output locations or specify supported alias behavior.

In Python, parameters bind object references; passing a list does not deep-copy it. State mutation/ownership, globals, result aliases, errors, and any copy-out policy in the contract. A caller cannot assume facts about untouched state unless a frame condition preserves it.

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.

Worked example: two output parameters alias one variable

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 procedures
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