Pre and Post Conditions: Hoare Logic

One way to specify and verify programs is by means of pre and post conditions. The main idea is that given a program or a function P, we write {pre} P {post}, where pre represents the precondition and post the postcondition.

This triple expresses the following: for any input, such that pre is satisfied (before executing P), when P is run, if it finishes its execution then post must hold.

Note that if the input does not satisfy pre, or if P does not end, then the triple is trivially satisfied

These are usually called Hoare triples, because of the article "An Axiomatic Basis for Computer Programming" [1].

For example,
{x \(\ge\) 0}
y := sqrt(x);
{y = \(\sqrt(x)\)}

This code only makes sense for non-negative x's, and after executing the statement y contains the square root of x.

These ideas are the basis of design by contract, where for each method there is a contract of what is expected about the input, and in case that holds, what is guaranteed about the output.

[1] Hoare, Charles Antony Richard. "An axiomatic basis for computer programming." Communications of the ACM 12, no. 10 (1969): 576-580.