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} .

Source: Wikipedia — Safety and liveness properties (CC BY-SA 4.0)