Predicative programming

EN Texte en anglais Pas encore d'article dans ta langue : extrait en anglais.

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...