Weakest Liberal Precondition

program-proofing

Definition

Weakest Liberal Precondition

The weakest liberal precondition (wlp) is the weakest formula such that the Hoare triple $\{\text{wlp}(\Pi ,G)\}\Pi \{G\}$ is partially correct.

Formal Semantics

In terms of the set of states $\mathcal{S}$, the wlp represents all states where the program $\Pi$ either fails to terminate or terminates in a state satisfying $G$:

$$\begin{array}{rl}\{\text{wlp}(\Pi ,G)\}& =\{\sigma \in \mathcal{S}\mid [\Pi ]\sigma \text{ undefined or }[\Pi ]\sigma \in \{G\}\}\\ & =\{\sigma \in \mathcal{S}\mid [\Pi ]\sigma \text{ undefined}\}\cup [\Pi {]}^{-1}(\{G\})\\ & =\{\sigma \in \mathcal{S}\mid [\Pi ]\sigma \text{ undefined}\}\cup \{\text{wp}(\Pi ,G)\}\end{array}$$

Correctness Relation

A specification $\{F\}\Pi \{G\}$ is partially correct if and only if $F$ is stronger than the weakest liberal precondition:

$$\begin{array}{rl}\{F\}\Pi \{G\}\text{ partially correct}& ⟺\{F\}\subseteq \{\text{wlp}(\Pi ,G)\}\\ & ⟺F⟹\text{wlp}(\Pi ,G)\text{ is valid}\end{array}$$

Base Cases

For the empty program, the wlp is simply the postcondition:

• $\text{wlp}(\mathbf{skip},G)=G$

Axiomatic Semantics

The wlp can be used to define the axiomatic semantics of a programming language (like SIMPLE) for partial correctness.