1 Answers
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 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 x {\displaystyle x} , y {\displaystyle y} , and z {\displaystyle z} , the command x {\displaystyle x} := y {\displaystyle y} +1 is equivalent to the specification x ′ {\displaystyle x'} = y {\displaystyle y} +1 ∧ y ′ {\displaystyle y'} = y {\displaystyle y} ∧ z ′ {\displaystyle z'} = z {\displaystyle z} in which x {\displaystyle x} , y {\displaystyle y} , and z {\displaystyle z} represent the values of the program variables before the assignment, and x ′ {\displaystyle x'} , y ′ {\displaystyle y'} , and z ′ {\displaystyle z'} represent the values of the program variables after the assignment. If the specification is x ′ {\displaystyle x'} > y {\displaystyle y} , we easily prove ⇒ , which says that x {\displaystyle x} := y {\displaystyle y} +1 implies, or refines, or implements x ′ {\displaystyle x'} > y {\displaystyle y}.
Loop proofs are greatly simplified. For example, if x {\displaystyle x} is an integer variable, to prove that
while x {\displaystyle x} >0 do x {\displaystyle x} := x {\displaystyle x} –1 od