Function init_invariant

pub proof fn init_invariant<T>(
    spec: TempPred<T>,
    init: StatePred<T>,
    next: ActionPred<T>,
    inv: StatePred<T>,
)

Expand description

requires

forall |s: T| #[trigger] init.apply(s) ==> inv.apply(s),

forall |s, s_prime: T| {
    inv.apply(s) && #[trigger] next.apply(s, s_prime) ==> inv.apply(s_prime)
},

spec.entails(lift_state(init)),

spec.entails(always(lift_action(next))),

ensures

spec.entails(always(lift_state(inv))),

Prove safety by induction.

init_invariant