Safety and liveness properties (original) (raw)

Properties of an execution of a computer program —particularly for concurrent and distributed systems— have long been formulated by giving safety properties ("bad things don't happen") and liveness properties ("good things do happen"). A simple example will illustrate safety and liveness. A program is totally correct with respect to a precondition and postcondition if any execution started in a state satisfying terminates in a state satisfying . Total correctness is a conjunction of a safety property and a liveness property: