Safety and liveness properties

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").^[1]

A program is totally correct with respect to a precondition ${\displaystyle P}$ and postcondition ${\displaystyle Q}$ if any execution started in a state satisfying ${\displaystyle P}$ terminates in a state satisfying ${\displaystyle Q}$. Total correctness is a conjunction of a safety property and a liveness property:^[2]

• The safety property prohibits these "bad things": executions that start in a state satisfying ${\displaystyle P}$ and terminate in a final state that does not satisfy ${\displaystyle Q}$. For a program ${\displaystyle C}$, this safety property is usually written using the Hoare triple ${\displaystyle \{P\}C\{Q\}}$.
• The liveness property, the "good thing", is that execution that starts in a state satisfying ${\displaystyle P}$ terminates.

Note that a bad thing is discrete,^[3] since it happens at a particular place during execution. A "good thing" need not be discrete, but the liveness property of termination is discrete.

Formal definitions that were ultimately proposed for safety properties^[4] and liveness properties^[5] demonstrated that this decomposition is not only intuitively appealing but is also complete: all properties of an execution are a conjunction of safety and liveness properties.^[5] Moreover, undertaking the decomposition can be helpful, because the formal definitions enable a proof that different methods must be used for verifying safety properties versus for verifying liveness properties.^[6][7]