Skip to main content

Module compositional

Module compositional 

Source
Expand description

Assume-Guarantee Compositional Reasoning

Decompose verification into per-component proofs with interface contracts. Each component has assumptions (what it requires from environment) and guarantees (what it provides). Verify each component independently.

Structs§

ComponentSpec
A component specification for compositional verification.

Enums§

CompositionalResult
Result of compositional verification.

Functions§

verify_compositional
Verify a set of components compositionally.