Predicative programming is the original name of a formal method for program specification and refinement, more recently called a Practical Theory of Programming, invented by Eric Hehner.
The central idea is that each specification is a binary (boolean) expression that is true of acceptable computer behaviors and false of unacceptable behaviors.
It follows that refinement is just implication.
This is the simplest formal method, and the most general, applying to sequential, parallel, stand-alone, communicating, terminating, nonterminating, natural-time, real-time, deterministic, and probabilistic programs, and includes time and space bounds.
Commands in a programming language are considered to be a special case of specification—those specifications that are compilable.
For example, if the program variables are
, the command
+1 is equivalent to the specification (binary expression)
represent the values of the program variables before the assignment, and
represent the values of the program variables after the assignment.
, we easily prove (
+1 implies, or refines, or implements
Loop proofs are greatly simplified.
is an integer variable, to prove that while
–1 od refines, or implements the specification
=0, prove if
fi ⇒ (
) is the empty, or do-nothing command.
There is no need for a loop invariant or least fixed point.
Loops with multiple intermediate shallow and deep exits work the same way.
This simplified form of proof is possible because program commands and specifications can be mixed together meaningfully.
Execution time (upper bounds, lower bounds, exact time) can be proven the same way, just by introducing a time variable.
To prove termination, prove the execution time is finite.
To prove nontermination, prove the execution time is infinite.
For example, if the time variable is
, and time is measured by counting iterations, then to prove that execution of the previous while-loop takes time
is initially nonnegative, and takes forever when
is initially negative, prove if
This formal methods-related article is a stub.
You can help Wikipedia by expanding it.