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 x {\displaystyle x} , y {\displaystyle y} , and z {\displaystyle z} , the command x {\displaystyle x} := y {\displaystyle y} +1 is equivalent to the specification (binary expression) 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 ( x {\displaystyle x} := y {\displaystyle y} +1) ⇒ ( x ′ {\displaystyle x'} > y {\displaystyle y} ), 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 refines, or implements the specification x {\displaystyle x} ≥0 ⇒ x ′ {\displaystyle x'} =0, prove if x {\displaystyle x} >0 then x {\displaystyle x} := x {\displaystyle x} –1; ( x {\displaystyle x} ≥0 ⇒ x ′ {\displaystyle x'} =0) else o k {\displaystyle ok} fi ⇒ ( x {\displaystyle x} ≥0 ⇒ x ′ {\displaystyle x'} =0) where o k {\displaystyle ok} = ( x ′ {\displaystyle x'} = x {\displaystyle x} ) 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 t {\displaystyle t} , and time is measured by counting iterations, then to prove that execution of the previous while-loop takes time x {\displaystyle x} when x {\displaystyle x} is initially nonnegative, and takes forever when x {\displaystyle x} is initially negative, prove if x {\displaystyle x} >0 then x {\displaystyle x} := x {\displaystyle x} –1; t {\displaystyle t} := t {\displaystyle t} +1; ( x {\displaystyle x} ≥0 ⇒ t ′ {\displaystyle t'} = t {\displaystyle t} + x {\displaystyle x} ) ∧ ( x {\displaystyle x} <0 ⇒ t ′ {\displaystyle t'} =∞) else o k {\displaystyle ok} fi ⇒ ( x {\displaystyle x} ≥0 ⇒ t ′ {\displaystyle t'} = t {\displaystyle t} + x {\displaystyle x} ) ∧ ( x {\displaystyle x} <0 ⇒ t ′ {\displaystyle t'} =∞) where o k {\displaystyle ok} = ( x ′ {\displaystyle x'} = x {\displaystyle x} ∧ t ′ {\displaystyle t'} = t {\displaystyle t} ).
… excerpt ends here. Continue reading the full article.
