SE463

• Temporal Connectives: – Henceforth (□): □f means f is true now and in all future states. – Eventually (♢): ♢f means f is true now or in some future state. – Next State (⃝): ⃝f means f is true in the next state. – Until (U): f U g means g will eventually be true, and f is true until then. – Unless (W): f W g means f is true indefinitely or until g becomes true (but g is not guaranteed to become true)

Correctness

1. strengthen the specification
2. strengthen the domain knowledge
3. weaken the requirement