Partially Correct Program (Hoare Calculus)

program-proofing

Definition

Partial Correctness

A program $\Pi$ is partially correct with respect to a precondition $P$ and a postcondition $Q$ if, for every execution that starts in a state satisfying $P$ and terminates, the resulting state satisfies $Q$.

In Hoare notation, this is written as:

$${\models }_{par}\{P\}\Pi \{Q\}$$

Formal Semantics

Using the set of states $\mathcal{S}$, we represent the set of states in which a formula $F$ is true as:

$$\{F\}=\{\sigma \in \mathcal{S}\mid [F]\sigma =1\}$$

A triple $\{F\}\Pi \{G\}$ is partially correct if for all $\sigma \in \mathcal{S}$:

$$[F]\sigma =1\wedge {\sigma }^{\prime }=[\Pi ]\sigma \text{ is defined}⟹[G]{\sigma }^{\prime }=1$$

Characteristics

• Non-Termination: Partial correctness does not guarantee that the program will actually finish. If a program enters an infinite loop, it is still vacuously partially correct for any postcondition, because there is no final state to violate the requirement.
• Safety Property: Partial correctness is often viewed as a safety property (“nothing bad happens”), whereas termination is a liveness property (“something good eventually happens”).

Verification

Proving partial correctness typically involves using the rules of the Hoare calculus, such as the composition rule and the assignment rule. For loops, a loop invariant must be identified.