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:

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)

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