Work sampling

Predicative programming is a methodology for program specification and refinement. The central idea of predicative programming is that each specification is a predicate (generally written as a boolean expression) that is true of acceptable behaviours and false of unacceptable behaviours. It follows that refinement is reversed implication universally quantified over behaviours:

$(P⊑Q)\equiv (\mathrm{\forall }b\cdot Q\Rightarrow P)$

Commands in a programming language are considered to be a special case of specifications—special only because they are compilable. For example in an environment where the program variables are $x$, $y$, and $z$, the command $x:=y+1$ is considered equivalent to the predicate (represented here by a boolean expression)

$x^{\prime }=y+1\wedge y^{\prime }=y\wedge z^{\prime }=z$

in which $x$, $y$, and $z$ represent the initial values of the program variables and $x^{\prime }$, $y^{\prime }$, and $z^{\prime }$ represent the final values of the program variables. Thus

$x^{\prime }>y⊑x:=y+1$

Bibliography

• E.C.R. Hehner, a Practical Theory of Programming, Springer-Verlag 1993. Most recent edition online at a Practical Theory of Programming.

External links

• Publications by Eric Hehner.