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

The Hoare calculus is a calculus for reasoning about the correctness of programs. It uses Hoare triples together with axioms and inference rules to show that a program transforms states satisfying a precondition into states satisfying a 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 of a program $\Pi$ and a postcondition $G$ is the most general (least restrictive) formula $\mathrm{wp}(\Pi ,G)$ such that the Hoare triple $\{\mathrm{wp}(\Pi ,G)\}\Pi \{G\}$ is totally correct.

Equivalently, $\mathrm{wp}(\Pi ,G)$ characterises exactly the states from which $\Pi$ terminates in a state satisfying $G$.

$$\{\mathrm{wp}(\Pi ,G)\}=\{\sigma \in \mathcal{S}\mid [\Pi ]\sigma \text{ is defined and }[G]([\Pi ]\sigma )=\text{true}\}$$

If a precondition $F$ implies $\mathrm{wp}(\Pi ,G)$, then $\{F\}\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 of a program $\Pi$ and a precondition $F$ is the most specific (most restrictive) formula $\mathrm{sp}(F,\Pi )$ such that the Hoare triple $\{F\}\Pi \{\mathrm{sp}(F,\Pi )\}$ is partially correct.

Equivalently, it is the set of states reached by executing $\Pi$ from states satisfying $F$:

$$\{\mathrm{sp}(F,\Pi )\}=\{[\Pi ]\sigma \mid \sigma \in \{F\}\text{ and }[\Pi ]\sigma \text{ is defined}\}$$ $$=[\Pi ](\{F\})$$

If a postcondition $G$ is implied by $\mathrm{sp}(F,\Pi )$, then $\{F\}\Pi \{G\}$ is partially correct.

Link to original