Unifying Theories of Reactive Design Contracts

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

what is proved or measured

Inference: The paper defines a UTP theory for stateful reactive design contracts and mechanizes its theorems in Isabelle/UTP. A contract has an assumption, an intermediate (pericondition) guarantee, and a terminating (postcondition) guarantee. The abstract says: “our theory of contracts allow us to specify both the evolution of state variables and the permissible interactions with the environment.” (abstract, p. 1) The theory uses alphabetized predicates, healthiness conditions, a generalized trace algebra, and relational operators. Its practical verification tactic reduces a contract refinement goal to three implications over pre-, peri-, and postconditions. The four contributions listed in section 1 (p. 2) are a UTP theory of stateful reactive contracts over a generalised trace model, a contract notation with assumptions and guarantees of intermediate and final states, theorems for calculating composite contracts including parallel composition, and an automated proof method for contractual refinement. The paper also works a cash-card case study (Section 5, pp. 22–25), which is not in that list.

technique: UTP relational encoding

Inference: What it is: represent programs and specifications as alphabetized predicates over initial and final observations. Refinement is implication under equal alphabets: P v Q means Q’s behaviors imply P’s. Sequential composition, choice, conditionals, assignment, and recursion are predicate operators. Definition 2.2 gives, for example, sequential composition through an existentially quantified intermediate state and assignment as a relation equating the post-state to the assigned value (section 2.1, p. 3).

Inference: When to use it: use this encoding when a reactive language needs a common semantic model and algebraic calculation laws. The abstract says the interaction model “supports, for instance, discrete time, continuous time, and hybrid computational models”, which the paper attributes to an abstract trace algebra (section 2.3, pp. 6–7) rather than a fixed list of events. The paper states: “UTP follows the “programs-as-predicates” approach [27], where a program is modelled as a relation in the alphabetised predicate calculus.” (section 2.1, p. 3)

Inference: How: (1) choose typed observational variables, including state and trace; (2) define healthiness conditions that restrict valid predicates; (3) define constructors as healthy operators; (4) express program behavior as predicates; (5) use relational laws to calculate compositions; (6) prove refinement by predicate implication in Isabelle/HOL. All theorems in the paper are mechanically proved in Isabelle/UTP (section 2, p. 2).

Inference: Verus form: model the state and logical trace with Verus spec fns and algebraic datatypes; express component contracts with requires and ensures; use proof functions to establish composition lemmas. Verus does not provide UTP alphabets, healthiness operators, or a built-in pericondition, so these must be represented explicitly in ghost state and predicates. This is a semantic translation, not a feature claimed by the paper.

technique: three-part reactive contract and refinement

Inference: What it is: Definition 4.1 defines [ P1 |− P2 | P3 ], where P1 is a reactive condition, P2 a reactive relation over intermediate observations, and P3 a reactive relation that may mention final state. Definition 4.1 defines the contract as Rs(P1 ⊢ P2 ◇ P3), a design made reactive by the healthiness condition Rs, where the diamond P2 ◇ P3 abbreviates P2 ◁ wait′ ▷ P3. Refinement is reduced by Theorem 4.2 to: precondition weakening, pericondition strengthening under the old precondition, and postcondition strengthening under the old precondition. The paper states: “Theorem 4.2 shows that contract refinement reduces to three proof obligations” (section 4.1, p. 13), namely P1 ⇒ Q1 for the precondition and the two strengthening obligations on periconditions and postconditions.

Inference: How: (1) calculate the program contract [Q1 |− Q2 | Q3]; (2) state the desired contract [P1 |− P2 | P3]; (3) prove P1 ⇒ Q1; (4) prove P2 v (Q2 ∧ P1); (5) prove P3 v (Q3 ∧ P1); (6) discharge the relational obligations with Isabelle/UTP tactics and, in Isabelle/HOL, the sledgehammer method that “harnesses external automated theorem provers” (section 4.1, p. 14). The three obligations are the paper’s (Theorem 4.2); the six-step ordering is this study’s summary of section 4.1 and the three-stage process of section 7 (pp. 36–37), which also uses the tactics rel-auto, rdes-simp and rdes-refine.

Inference: Verus form: write one Verus lemma per implication, with requires encoding the specification assumption and ensures encoding each guarantee. A terminating method can model P3; intermediate observations require a ghost event/trace model and separate lemmas. Verus’s ensures can express final-state guarantees but does not directly encode a reactive design’s waiting observation.

technique: algebraic contract composition

Inference: What it is: Theorem 4.13 supplies laws for internal choice, indexed choice, conjunction, conditionals, sequential composition, and iteration. The sequential composition law (4.13.5) gives precondition P1 ∧ (P3 wlp_r Q1), that is, the first precondition conjoined with the reactive weakest liberal precondition, over the first postcondition, of the second precondition; pericondition P2 ∨ (P3 ; Q2); and postcondition P3 ; Q3. Law 4.13.6 gives the finite iteration [P |− Q | R]^(n+1), and Theorem 4.15 gives the contract of the tail recursion µR X • [P |− Q | R] ; X when R is productive (R4-healthy), with a false postcondition. The paper says: “These are theorems, rather than definitions, since they formulate the semantics of contracts that are composed by the UTP operators defined previously in Definition 2.2.” (section 4.3, p. 17)

Inference: When to use it: calculate a system contract compositionally before proving a system-level property. The paper says calculated contracts “are symbolic rather than explicit entities, which allows us to overcome the state explosion problem” (section 4.1, p. 14).

Inference: Verus form: create reusable proof lemmas for sequential contract composition and state-update frame properties. A Rust method’s executable body remains ordinary Rust; the algebra lives in proof fns and spec fns. The UTP operators’ exact equations do not carry over unless a trace model is implemented.

technique: contract-based case-study verification

Inference: The card system defines Pay(i,j,n), rejects invalid transfers, performs two indexed assignments for valid transfers, and iterates an internal choice over card pairs. The paper states Theorem 5.4, which calculates the P1/P2/P3 contract of Pay, as proved “by use of our tactics in Isabelle/UTP”, then verifies three refinements with rdes-refine: no change in total balance (Theorem 5.5), no overdrafts (Theorem 5.6), and acceptance of a valid transfer (Theorem 5.7). The proofs printed in the paper are high-level informal arguments that correspond to the mechanised ones (section 5, p. 24). The paper states: “Each of these properties is assigned a contract which Pay(i, j, n) must refine.” (section 5, p. 24)

Inference: How: calculate the Pay contract; state each property as a contract; invoke the refinement tactic; for balance preservation, split the postcondition into invalid-transfer (state unchanged) and valid-transfer (subtract n then add n) cases; for no overdraft, split the affected index into i, j, and all other cards; for acceptance, reason over the pericondition and case-split the possible intermediate observations.

Inference: Verus form: represent balances as a map or sequence with a view, specify transfer preconditions and postconditions, and prove sum preservation and non-negativity by case analysis. Use old state in ensures; use assert and arithmetic proof blocks for the i/j/other-index cases. Reactive event offers and periconditions require ghost traces and are not directly executable Verus behavior.

techniques for the catalog

• UTP predicate semantics — encode programs as alphabetized predicates constrained by healthiness conditions
• three-obligation contract refinement — reduce refinement to precondition, pericondition, and postcondition implications
• algebraic contract composition — calculate composite assumptions and guarantees with proved relational laws
• reactive case-study proof — verify stateful protocols by contract refinement and index-based postcondition case analysis

Last edited: 2026-10-17