Go backward to More About Invariance Proofs Go up to Top Go forward to Example

Eventuality Properties

• Something eventually happens.
• Termination
  • eventually terminated.
• Service
  • If process has requested service, it is eventually served.
  • requested |-> served.
• Message delivery
  • If a message is sent often enough, it is eventually delivered.
  • (always eventually sent) => eventually delivered.
• P |-> Q.
  • Phi and (n in Nat) => eventually (x>n)
  • Phi =>((n in Nat and x=n) |-> eventually (x=n+1))

Must be derived from fairness condition!