always_weaken

vstd_extra::temporal_logic::rules

Function always_weaken 

Source 
pub proof fn always_weaken<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>)
Expand description
requires
valid(p.implies(q)),
spec.entails(always(p)),
ensures
spec.entails(always(q)),

Weaken □ by ⇒.

§Preconditions

  • ⊧ p ⇒ q
  • spec ⊧ □p

§Postconditions

  • spec ⊧ □q