transform_leads_to_with_until

vstd_extra::temporal_logic::rules

Function transform_leads_to_with_until 

Source 
pub proof fn transform_leads_to_with_until<T>(
    spec: TempPred<T>,
    next: TempPred<T>,
    p1: TempPred<T>,
    q1: TempPred<T>,
    p2: TempPred<T>,
    q2: TempPred<T>,
)
Expand description
requires
spec.entails(p1.leads_to(q1)),
spec.entails(always(p2.and(next).implies(later(p2).or(later(q2))))),
spec.entails(always(next)),
ensures
spec.entails(p1.and(p2).leads_to((q1.and(p2)).or(q2))),

Get a new ⇝ condition with an until condition.

This lemma can be used in compositional proof. Suppose that a system consists of two concurrent components A and B, and we want to prove that the entire system makes P1 ⇝ P3. If we have already proved that (1) A makes P1 ⇝ P2 hold, and (2) P2 holds until P3 holds, and (3) if P2 holds until P3 holds, then B makes P2 ⇝ P3 (in other words, B requires that P2 should hold until B makes P3 hold), then we can apply this lemma and prove that the entire system makes P2 ⇝ P3, then by transitivity we have P1 ⇝ P3.

Such a case could happen between components with liveness dependencies: A at some point needs to delegate the task to B and A needs to wait until B finish so A can start the next task, meanwhile when B is working A should not disable B’s progress (i.e., A should make sure P2 holds until P3 holds).

§Preconditions

  • spec ⊧ p1 ⇝ q1
  • spec ⊧ □(p2 ∧ next ⇒ p2' ∨ q2')
  • spec ⊧ □next

§Postconditions

  • spec ⊧ p1 ∧ p2 ⇝ (q1 ∧ p2) ∨ q2