strengthen_leads_to_with_until

vstd_extra::temporal_logic::rules

Function strengthen_leads_to_with_until 

Source 
pub proof fn strengthen_leads_to_with_until<T>(
    spec: TempPred<T>,
    next: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
)
Expand description
requires
spec.entails(always(p).leads_to(q)),
spec.entails(always(p.and(next).implies(later(p).or(later(q))))),
spec.entails(always(next)),
ensures
spec.entails(p.leads_to(q)),

Derive p ⇝ q from □p ⇝ q with the assumption that p is preserved unless q happens.

This lemma is useful if we want to show that given □p ⇝ q, q will eventually hold even if □p doesn’t hold, as long as p is preserved until q happens. A concrete usage is to reason about a pair of concurrent components A and B, where (1) A guarantees □p ⇝ q, and (2) B makes p hold at some point and keeps p until q holds. Note that we formalize “p is preserved until q happens” using □(p ∧ next ⇒ p' ∨ q'): if p holds now, then for any possible next state, either p or q holds.

§Preconditions

  • spec ⊧ □p ⇝ q
  • spec ⊧ □(p ∧ next ⇒ p' ∨ q')
  • spec ⊧ □next

§Postconditions

  • spec ⊧ p ⇝ q