Partially Correct Program

program-proofing

Definition

Partially Correct Program

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

In Hoare notation, this is written as:

Formal Semantics

Using the set of states , we represent the set of states in which a formula is true as:

A triple is partially correct if for all :

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.