strengthen_next

vstd_extra::temporal_logic::rules

Function strengthen_next 

Source 
pub proof fn strengthen_next<T>(
    spec: TempPred<T>,
    next: ActionPred<T>,
    inv: StatePred<T>,
    next_and_inv: ActionPred<T>,
)
Expand description
requires
spec.entails(always(lift_action(next))),
spec.entails(always(lift_state(inv))),
lift_action(next_and_inv).entails(lift_action(next).and(lift_state(inv))),
lift_action(next).and(lift_state(inv)).entails(lift_action(next_and_inv)),
ensures
spec.entails(always(lift_action(next_and_inv))),

Strengthen next with inv.

§Preconditions

  • spec ⊧ □next
  • spec ⊧ □inv
  • ⊧ next ∧ inv <=> next_and_inv

§Postconditions

  • spec ⊧ □next_and_inv