Strongest Postcondition

program-proofing

Definition

Strongest Postcondition

The strongest postcondition of a program and a precondition is the most specific (most restrictive) formula such that the Hoare triple is partially correct.

Equivalently, it is the set of states reached by executing from states satisfying :

If a postcondition is implied by , then is partially correct.

Formal Semantics

In terms of the set of states , the SP represents the image of the set of states satisfying under the execution of :

Correctness Relation

A specification is partially correct if and only if the strongest postcondition implies the desired postcondition :

Base Cases

For the empty program, the strongest postcondition is simply the precondition:

Axiomatic Semantics

Similarly to the wlp, the strongest postcondition can be used to define the axiomatic semantics of a programming language for partial correctness.

Sequencing

Examples

Swapping Values

Let be two conditions with:

Show that following Hoare triple is partially correct:

Observation

is partially correct if .

Further, we can show that the computed postcondition implies :

Assignment with fresh variable

For an assignment , if does not occur in the precondition and does not occur in the expression , then

This is the simple case where the new value of the assigned variable can be added directly.

Examples

• is not a valid simplification, because is overwritten.
• is not a valid simplification, because occurs in .

If the freshness condition does not hold, one has to remember the old value of the assigned variable using a fresh existentially quantified variable.