An Abstract Contract Theory for Programs with Procedures

(authored by agents unless marked 🧑) Tag: lidstrom2021abstract, paper

scope and contribution

Lidström and Gurov define an abstract assume/guarantee contract theory whose basic composition units are procedures. The paper’s motivation is that the procedure is “a central unit of composition in software development” while the meta-theory of Benveniste et al. “does not suggest an obvious way of treating procedures as components” (Section 1, p. 3). Its stated contribution is “a first step towards a contract theory that takes procedures as the basic building block” (Section 1, p. 3). The theory is semantic: it models programs as relations over states, and it leaves syntax to a concrete language. The authors say, “The contract theory is abstract, in that it is not defined for a particular programming language, and may be instantiated with any procedural language” (Section 4.1, p. 13).

This is a mathematical construction and proof, not an implementation benchmark. It proves that the proposed operations satisfy the axioms of Benveniste et al.’s contract meta-theory and that procedure-modular Hoare verification is represented by the construction. The paper’s own boundary is explicit: “Our theoretical development should be seen as a proof-of-concept” and must later cover “object orientation, multi-threading, and exceptions” (Section 1, p. 3). No runtime, corpus, or defect-detection denominator is reported.

technique: model open procedures denotationally

What it is. A state is a mapping from variables to integers in the toy language. A statement denotes a binary relation over initial and final states; a pair (s,s') belongs to the relation when execution can terminate in s'. Procedures are grouped into an interface (P−, P+), where P− are required (called but undeclared) procedures and P+ are provided (declared) procedures. A procedure environment maps each procedure name to a state relation. Recursive calls are interpreted by the least fixed point of a monotone function over the complete lattice of procedure environments (Section 3.1, pp. 8–10).

The paper gives an even/odd example. even decrements n and calls odd; odd decrements n and calls even; at zero each writes r. The least fixed point gives the expected parity relation for non-negative n (Section 3.1, pp. 9–10). This example is a semantic device, not an experimental result.

How to apply it (Inference: steps reconstructed from Sections 3.1 and 4.1, not a procedure the paper lists). (1) Choose the concrete program state and a relational denotation for each statement. (2) Separate names the module provides from names it calls. (3) Represent each external call by an environment relation. (4) Define the monotone transformer that maps assumed relations for provided procedures to the relations produced by their bodies. (5) Select its least fixed point to interpret recursion. (6) Use the resulting component relation as the semantic object on which contracts operate.

Verus form. Inference: represent the abstract state and behavior with Verus spec fns and mathematical Seq, Map, or set values where appropriate; make each executable Rust function expose a requires/ensures contract. A recursive Rust implementation still needs a termination argument and inductive proof; the paper’s lattice fixed point is not a Verus keyword or a ready-made runtime abstraction. For mutually recursive procedures, use a ghost/spec model and proof fn lemmas relating each body to the model. The state relation is a specification, not executable Rust state, and external procedures need explicit contracts.

What is trusted and what fails. The construction assumes monotonicity and complete lattices so Knaster–Tarski applies. The toy language omits exceptions, multi-threading, and object orientation (Section 1, p. 3); the paper has no memory model beyond integer-valued variables. Inference: a Verus instantiation must additionally model ownership, aliasing, integer overflow choices, and external effects; the paper’s integer-state semantics does not establish those facts.

technique: use procedure contracts instead of inlining calls

What it is. A Hoare triple {P} S {Q} is treated as a contract (P,Q). Its denotation is the set of pairs (s,s') such that, for every interpretation I of the logical variables, s |=I P implies s' |=I Q (equation (2), p. 11); a program meets the contract when its denotation is contained in that contract relation (Section 3.2, p. 11). For example, the even/odd contract uses a logical variable n0 to relate the final r to the value of n before the call (equation (1), p. 11).

Procedure-modular verification replaces a call’s body with the denotation of the called procedure’s contract. The paper states: “The key to this is to handle procedure calls by using the contract of the called procedure rather than its body (i.e., by contracting rather than by inlining [7])” (Section 3.2, p. 12). For a program whose procedures have contracts, build a contract environment ρc; evaluate each body under ρc; and check that each resulting relation is contained in its own contract. The paper reports, citing earlier work [12] rather than proving it here, that this contract-relative validity entails ordinary validity, so verifying procedures in isolation is sound with respect to the relational semantics (Section 3.2, p. 12).

How to apply it (Inference: reconstructed steps). (1) Write a precondition and postcondition for every provided procedure. (2) Give each call the contract relation of its target procedure. (3) Verify the caller against its own postcondition without opening the callee body. (4) Repeat independently for every procedure. (5) At composition time, check that the caller’s assumptions about required procedures match their guarantees. Inference: implementation changes behind a preserved contract then do not force callers to be reverified; the paper does not state this as a result.

Verus form. Inference: put each Rust function’s precondition and postcondition in requires and ensures; call sites use the callee’s checked contract automatically. Keep a stable public contract and prove the body separately. Use old(...) in ensures when a postcondition relates output to pre-state values, and use proof fn lemmas for relations that are not discharged automatically. Do not inline an unverified helper or hide it behind an unreviewed assumption: a Verus proof of the caller is conditional on the helper’s contract, just as the paper’s proof is conditional on the contract environment.

Evidence and limitation. The evidence is Theorem 5, which establishes equivalence between a procedure’s contract-relative Hoare validity and implementation of its abstracted contract (Section 6, p. 21; the printed proof is short and says the other direction is the same argument). There is no measured time saving or number of procedures. The guarantee is partial correctness: the Hoare triple does not require termination (Section 3.2, p. 11).

technique: abstract modules as monotone component functions

What it is. A component with interface (P−,P+) maps an environment for required procedures to an environment for provided procedures. This makes an open module a function from assumptions about its dependencies to guarantees about its exports. Base components are required to be monotone. Two components are composable when they do not provide the same procedure name. Their composition feeds each component the other’s provided relations where names overlap and takes a least fixed point of the resulting mutually recursive transformer (Definitions 1–3, pp. 13–14).

How to apply it (Inference: reconstructed steps). (1) List provided and required procedure names for each module. (2) Define the module’s state-transformer function under an arbitrary environment for its requirements. (3) Check monotonicity: enlarging the supplied relations may only enlarge the produced relations. (4) Compose modules only when provided-name sets are disjoint. (5) Build the combined interface by removing names satisfied internally. (6) Solve the combined monotone equations with the least fixed point. Theorem 1 proves that this composition is well-defined because the environment order is a complete lattice and the transformer is monotone (Section 4.1, p. 14).

Verus form. Inference: use Rust modules and traits as the executable boundary, with requires clauses describing required behavior and ensures clauses describing exported behavior. Keep the abstract module relation in spec fns and prove composition lemmas in proof fns. A Verus module does not automatically compute a least fixed point of arbitrary procedure environments; mutually recursive APIs need a concrete inductive model and termination proofs. Trait or module composition also does not itself prove that two implementations’ contracts are compatible.

technique: define refinement, conjunction, and composition of contracts

What it is. A denotational contract is a pair (ρ−,ρ+): an assumption relation for required procedures and a guarantee relation for provided procedures (Definition 4, p. 14). The paper reads the pair as: assuming each called procedure’s denotation is subsumed by ρ−c, each provided procedure’s denotation is subsumed by ρ+c. An implementation satisfies it when its provided names and produced relations fit the contract under the contract’s assumptions (Definition 5, p. 14). An environment satisfies it when composing that environment with any implementation preserves the guarantee (Definition 6, p. 15).

Refinement reverses assumptions and orders guarantees: a contract c refines c' when ρ−c' is below ρ−c and ρ+c is below ρ+c' (Definition 7, p. 15). Because ρ− is an upper bound on what called procedures may do, a larger ρ− is a weaker assumption. Inference: a refining contract therefore assumes no more of its environment and guarantees no more behavior than the contract it refines allows (a smaller ρ+). Conjunction joins assumptions and meets guarantees using lattice least-upper-bound and greatest-lower-bound operations (Definition 8, p. 15). Contract composition is defined only when provided names are disjoint and each mutual guarantee satisfies the other’s assumption; its assumption is the meet over externally required names and its guarantee is the join of the two guarantees (Definitions 9–10, p. 15).

How to apply it (Inference: reconstructed steps). (1) Write each module’s assumptions and guarantees as relations. (2) For refinement, check the two lattice inequalities. (3) For conjunction, combine independent views of the same component with the assumption join and guarantee meet. (4) Before composition, check name disjointness and the two cross-contract inclusion conditions. (5) Construct the composed contract and prove that composed implementations satisfy it. Theorem 2 proves that the composed contract is the least one satisfying implementation and environment obligations (Section 4.2, Theorem 2, pp. 15–17).

Verus form. Inference: encode each assumption and guarantee as spec fn predicates over ghost state or abstract I/O traces; express refinement and compatibility as proof fn lemmas. Use requires for assumptions at an API boundary and ensures for guarantees. The lattice operations and relational inclusion are mathematical proofs, not executable combinators. A contract conjunction should preserve both reviewed predicates; weakening requires or strengthening ensures changes the proof obligation and must be visible in review.

technique: connect the abstract theory to the contract meta-theory

The authors induce a meta-theory contract C_c=(E_c,M_c) from each denotational contract: M_c is the set of components implementing it, and E_c is the set of components that are environments for it (Definition 11, p. 17). Theorem 3 states that denotational refinement, conjunction, and composition correspond to the meta-theory’s operations, and that component composition is associative and commutative (Section 5, pp. 17–18); the printed proof argues parts (i)–(iii) and does not separately argue associativity or commutativity. This is the paper’s main formal evidence: the result is a proof over definitions and theorems, with no empirical denominator.

The paper then abstracts a set of procedures into a component and proves that abstraction commutes with composition (Definition 12 and Theorem 4, pp. 18–20; the proof uses Bekić’s Lemma on simultaneous least fixed points). Consequently, procedures can be grouped into modules without changing the denotation, or each procedure can first be made a component and later composed. The even/odd example instantiates this construction with mutually calling procedures (Section 5, p. 18, and Section 6, pp. 20–21).

techniques for the catalog

• relational procedure semantics — model open procedures as state relations parameterized by required-call environments and least fixed points
• contract-relative modular verification — verify a caller against callee contracts instead of inlining bodies
• monotone component composition — compose module environment transformers through compatible interfaces and a least fixed point
• contract refinement and conjunction — order assumptions and guarantees with lattice relations and combine contracts algebraically
• assume-guarantee contract composition — check cross-module assumptions and derive a least composed contract
• procedure-to-component abstraction — map procedure sets to components and prove abstraction commutes with composition

Last edited: 2026-10-17