wf1_by_borrowing_inv

vstd_extra::temporal_logic::rules

Function wf1_by_borrowing_inv 

Source 
pub proof fn wf1_by_borrowing_inv<T>(
    spec: TempPred<T>,
    next: ActionPred<T>,
    forward: ActionPred<T>,
    p: StatePred<T>,
    q: StatePred<T>,
    inv: StatePred<T>,
)
Expand description
requires
forall |s, s_prime: T| {
    p.apply(s) && inv.apply(s) && #[trigger] next.apply(s, s_prime)
        ==> p.apply(s_prime) || q.apply(s_prime)
},
forall |s, s_prime: T| {
    p.apply(s) && inv.apply(s) && #[trigger] next.apply(s, s_prime)
        && forward.apply(s, s_prime) ==> q.apply(s_prime)
},
forall |s: T| #[trigger] p.apply(s) && inv.apply(s) ==> enabled(forward).apply(s),
spec.entails(always(lift_action(next))),
spec.entails(always(lift_state(inv))),
spec.entails(weak_fairness(forward)),
ensures
spec.entails(lift_state(p).leads_to(lift_state(q))),

Get the initial ⇝ with a stronger wf assumption by borrowing existing inv.

§Preconditions

  • ⊧ p ∧ inv ∧ next ⇒ p' ∨ q'
  • ⊧ p ∧ inv ∧ next ∧ forward ⇒ q'
  • ⊧ p ∧ inv ⇒ enabled(forward)
  • spec ⊧ □lift_action(next)
  • spec ⊧ □lift_state(inv)
  • spec ⊧ wf(forward)

§Postconditions

  • spec ⊧ p ⇝ q