Contract-Based Design

Assume-guarantee contracts for subsystem composition. This module addresses the most common cause of emergent failure: implicit assumptions that are not discharged by any other subsystem's guarantees.

A Contract carries a formal proof that its assumption implies its guarantee. A list of contracts is CompositionSound when every contract's assumption is entailed by the conjunction of other contracts' guarantees (plus a base environmental assumption). This check is a type-level obligation, so missing assumptions surface at build time rather than at integration.

Design Notes

• Contract.valid is the local proof assume → guarantee.
• CouplingConstraint captures properties that genuinely cross subsystem boundaries and cannot be expressed as a local per-subsystem invariant.
• The composition check uses logical implication rather than syntactic equality on propositions, which sidesteps the lack of DecidableEq Prop.

structure VerifiedMBSE.VV.Contract : Type

Contract: subsystem-level assume-guarantee pair with a validity proof.

• name : String

  Contract identifier (used for traceability and diagnostics).

• assume : Prop

  What the subsystem requires from its environment.

• guarantee : Prop

  What the subsystem guarantees in return.

• valid : self.assume → self.guarantee

  Local validity: if the assumption holds, so does the guarantee.

def VerifiedMBSE.VV.Contract.compose (c₁ c₂ : Contract) (link : c₁.guarantee → c₂.assume) : Contract

Sequential composition of two contracts. If c₁.guarantee entails c₂.assume, the composed contract has c₁.assume as its assumption and c₂.guarantee as its guarantee.

Equations

• c₁.compose c₂ link = { name := c₁.name ++ " ∘ " ++ c₂.name, assume := c₁.assume, guarantee := c₂.guarantee, valid := ⋯ }

structure VerifiedMBSE.VV.DischargedContract : Type

A contract whose assumption has been explicitly discharged.

• contract : Contract

  The underlying contract.

• assumption_proof : self.contract.assume

  Proof that the contract's assumption holds.

theorem VerifiedMBSE.VV.DischargedContract.guarantee_holds (dc : DischargedContract) : dc.contract.guarantee

The guarantee of a discharged contract is provable.

structure VerifiedMBSE.VV.CouplingConstraint : Type

CouplingConstraint: a cross-cutting property that involves multiple subsystems and is not reducible to any single subsystem's invariant. Examples include total power budget, mass budget, thermal coupling, electromagnetic compatibility, and communication-link budgets.

• name : String

  Constraint identifier.

• involved : List String

  Names of subsystems participating in this constraint.

• property : Prop

  The cross-cutting property.

• evidence : self.property

  Proof that the property holds.

def VerifiedMBSE.VV.CouplingConstraint.arity (cc : CouplingConstraint) : Nat

Number of subsystems a constraint couples.

Equations

• cc.arity = cc.involved.length

structure VerifiedMBSE.VV.ContractedSystem : Type

ContractedSystem: a set of contracts together with coupling constraints and a proof that every contract's assumption has been discharged.

• contracts : List Contract

  All subsystem contracts.

• couplings : List CouplingConstraint

  Cross-cutting coupling constraints.

• discharged (c : Contract) : c ∈ self.contracts → c.assume

  Every contract assumption is discharged. Constructing this system requires producing a proof for each assumption — this is where the integration story becomes machine-checked.

theorem VerifiedMBSE.VV.ContractedSystem.guarantees_hold (cs : ContractedSystem) (c : Contract) : c ∈ cs.contracts → c.guarantee

Every contract's guarantee holds in a well-formed contracted system.

def VerifiedMBSE.VV.ContractedSystem.contractCount (cs : ContractedSystem) : Nat

Number of contracts in a contracted system.

Equations

• cs.contractCount = cs.contracts.length

def VerifiedMBSE.VV.ContractedSystem.couplingCount (cs : ContractedSystem) : Nat

Number of coupling constraints in a contracted system.

Equations

• cs.couplingCount = cs.couplings.length