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").

A program is totally correct with respect to a precondition

P

{\displaystyle P}

and postcondition

Q

{\displaystyle Q}

if any execution started in a state satisfying

P

{\displaystyle P}

terminates in a state satisfying

Q

{\displaystyle Q}

. Total correctness is a conjunction of a safety property and a liveness property:

The safety property prohibits these "bad things": executions that start in a state satisfying

P

{\displaystyle P}

and terminate in a final state that does not satisfy

Q

{\displaystyle Q}

. For a program

C

{\displaystyle C}

, this safety property is usually written using the Hoare triple

{

P

}

C

{

Q

}

{\displaystyle \{P\}C\{Q\}}

.

The liveness property, the "good thing", is that execution that starts in a state satisfying

P

{\displaystyle P}

terminates.

Note that a bad thing is discrete, 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 and liveness properties 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. 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.

Safety

A safety property proscribes discrete bad things from occurring during an execution.