Predicative programming

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\sqsubseteq Q)\equiv (\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'=y+1\land y'=y\land z'=z$

in which $x$, $y$, and $z$ represent the initial values of the program variables and $x'$, $y'$, and $z'$ represent the final values of the program variables. Thus

$x'>y\sqsubseteq 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.