Program Proofing

program-proofing

Definition

Program Proofing

Program proofing (or program verification) is the formal process of proving that a program $\Pi$ is correct with respect to a formal specification.

Methods

Hoare Calculus

Decompose correctness assertions into simpler ones using inference rules until only true statements and valid formulas remain. This method uses the Hoare calculus directly.

Definition

Hoare Calculus

Hoare calculus is a formal system used to reason about the correctness of programs. It uses a set of axioms and inference rules to prove that if a program starts in a state satisfying a specific condition (precondition), it will end in a state satisfying another condition (postcondition).

Link to original

Weakest Precondition

Calculate the weakest formula $F^{\prime }$ such that $\{F^{\prime }\}\Pi \{G\}$ holds, and show that the given precondition $F$ implies $F^{\prime }$.

Definition

Weakest Precondition

The weakest precondition (WP) is the most general (least restrictive) formula $F^{\prime }$ such that the Hoare triple $\{F^{\prime }\}\Pi \{G\}$ is totally correct.

Link to original

Strongest Postcondition

Calculate the strongest formula $G^{\prime }$ such that $\{F\}\Pi \{G^{\prime }\}$ holds, and show that $G^{\prime }$ implies the desired postcondition $G$.

Definition

Strongest Postcondition

The strongest postcondition (SP), denoted as $\text{sp}(F,\Pi )$, is the most specific (most restrictive) formula $G^{\prime }$ such that the Hoare triple $\{F\}\Pi \{G^{\prime }\}$ is partially correct.

Formal Semantics

In terms of the set of states $\mathcal{S}$, the SP represents the image of the set of states satisfying $F$ under the execution of $\Pi$:

$$\begin{array}{rl}\{\text{sp}(F,\Pi )\}& =\{[\Pi ]\sigma \mid \sigma \in \{F\}\text{ and }[\Pi ]\sigma \text{ defined}\}\\ & =[\Pi ](\{F\})\end{array}$$ Link to original