Predicative programming
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 , , and , the command := +1 is equivalent to the specification (binary expression) =+1 ∧ = ∧ = in which , , and  represent the values of the program variables before the assignment, and  , , and  represent the values of the program variables after the assignment. If the specification is >, we easily prove (:= +1) ⇒ (>), which says that := +1 implies, or refines, or implements >. Loop proofs are greatly simplified. For example, if  is an integer variable, to prove that

	while >0 do := –1 od

refines, or implements the specification ≥0 ⇒ =0, prove

	if >0 then := –1; (≥0 ⇒ =0) else  fi  ⇒  (≥0 ⇒ =0)

where    =  (=) 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  when  is initially nonnegative, and takes forever when  is initially negative, prove

	     if >0 then := –1; := +1; (≥0 ⇒ =+) ∧ (<0 ⇒ =∞) else  fi
	⇒  (≥0 ⇒ =+) ∧ (<0 ⇒ =∞)

where    =   (= ∧ =). 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. Formal methods
Formal specification languages
Logical calculi