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. A safety property thus characterizes what is permitted by stating what is prohibited. The requirement that the bad thing be discrete means that a bad thing occurring during execution necessarily occurs at some identifiable point. Examples of a discrete bad thing that could be used to define a safety property include:
An execution that starts in a state satisfying a given precondition terminates, but the final state does not satisfy the required postcondition; An execution of two concurrent processes, where the program counters for both processes designate statements within a critical section; An execution of two concurrent processes where each process is waiting for another to change state (known as deadlock). An execution of a program can be described formally by giving the infinite sequence of program states that results as execution proceeds, where the last state for a terminating program is repeated infinitely. For a program of interest, let S {\displaystyle S} denote the set of possible program states, S ∗ {\displaystyle S^{*}} denote the set of finite sequences of program states, and S ω {\displaystyle S^{\omega }} denote the set of infinite sequences of program states. The relation σ ≤ τ {\displaystyle \sigma \leq \tau } holds for sequences σ {\displaystyle \sigma } and τ {\displaystyle \tau } iff σ {\displaystyle \sigma } is a prefix of τ {\displaystyle \tau } or σ {\displaystyle \sigma } equals τ {\displaystyle \tau } . A property of a program is the set of allowed executions. The essential characteristic of a safety property S P {\displaystyle SP} is: If some execution σ {\displaystyle \sigma } does not satisfy S P {\displaystyle SP} then the defining bad thing for that safety property occurs at some point in σ {\displaystyle \sigma } . Notice that after such a bad thing, if further execution results in an execution
σ ′ {\displaystyle \sigma ^{\prime }} , then σ ′ {\displaystyle \sigma ^{\prime }} also does not satisfy S P {\displaystyle SP} , since the bad thing in σ {\displaystyle \sigma } also occurs in σ ′ {\displaystyle \sigma ^{\prime }} . We take this inference about the irremediability of bad things to be the defining characteristic for S P {\displaystyle SP} to be a safety property. Formalizing this in predicate logic gives a formal definition for S P {\displaystyle SP} being a safety property.
∀ σ ∈ S ω : σ ∉ S P ⟹ ( ∃ β ≤ σ : ( ∀ τ ∈ S ω : β τ ∉ S P ) ) {\displaystyle \forall \sigma \in S^{\omega }:\sigma \notin SP\implies (\exists \beta \leq \sigma :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))}
… excerpt ends here. Continue reading the full article.
