Skip to main content

verify_compositional

Function verify_compositional 

Source
pub fn verify_compositional(components: &[ComponentSpec]) -> CompositionalResult
Expand description

Verify a set of components compositionally.

For each component:

  1. Assume all assumptions hold
  2. Verify all guarantees under those assumptions
  3. Check that each component’s guarantees discharge other components’ assumptions