implies_new_invariant

vstd_extra::temporal_logic::rules

Function implies_new_invariant 

Source 
pub proof fn implies_new_invariant<T>(
    spec: TempPred<T>,
    init: StatePred<T>,
    next: ActionPred<T>,
    inv: StatePred<T>,
    proved_inv: StatePred<T>,
)
Expand description
requires
forall |s: T| #[trigger] init.apply(s) ==> inv.apply(s),
forall |s, s_prime: T| {
    inv.apply(s) && proved_inv.apply(s) && #[trigger] next.apply(s, s_prime)
        ==> inv.apply(s_prime)
},
spec.entails(lift_state(init)),
spec.entails(always(lift_action(next))),
spec.entails(always(lift_state(proved_inv))),
ensures
spec.entails(always(lift_state(inv))),

Implies new invariant from proved invariant by induction.

§Preconditions

  • ⊧ init ⇒ inv
  • ⊧ inv ∧ proved_inv ∧ next ⇒ inv'
  • spec ⊧ init ∧ □next ∧ □proved_inv

§Postconditions

  • spec ⊧ □inv