This articlerelies largely or entirely on asingle source. Relevant discussion may be found on thetalk page. Please helpimprove this article byintroducing citations to additional sources. Find sources: "Predicative programming" – news ·newspapers ·books ·scholar ·JSTOR(June 2024)

This article includes alist of references,related reading, orexternal links,but its sources remain unclear because it lacksinline citations. Please helpimprove this article byintroducing more precise citations.(June 2024) (Learn how and when to remove this message)

Predicative programming is the original name of a formal method for programspecification andrefinement, more recently called a Practical Theory of Programming, invented byEric 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 justimplication. This is the simplest formal method, and the most general, applying to sequential, parallel, stand-alone, communicating, terminating, nonterminating, natural-time, real-time, deterministic, andprobabilistic programs, and includes time and space bounds.

Commands in aprogramming language are considered to be a special case of specification—those specifications that are compilable. For example, if the program variables are${\displaystyle x}$,${\displaystyle y}$, and${\displaystyle z}$, the command${\displaystyle x}$:=${\displaystyle y}$+1 is equivalent to the specification (binary expression)${\displaystyle x^{\prime }}$=${\displaystyle y}$+1 ∧${\displaystyle y^{\prime }}$=${\displaystyle y}$ ∧${\displaystyle z^{\prime }}$=${\displaystyle z}$ in which${\displaystyle x}$,${\displaystyle y}$, and${\displaystyle z}$ represent the values of the program variables before the assignment, and${\displaystyle x^{\prime }}$,${\displaystyle y^{\prime }}$, and${\displaystyle z^{\prime }}$ represent the values of the program variables after the assignment. If the specification is${\displaystyle x^{\prime }}$>${\displaystyle y}$, we easily prove (${\displaystyle x}$:=${\displaystyle y}$+1) ⇒ (${\displaystyle x^{\prime }}$>${\displaystyle y}$), which says that${\displaystyle x}$:=${\displaystyle y}$+1 implies, or refines, or implements${\displaystyle x^{\prime }}$>${\displaystyle y}$.

Loop proofs are greatly simplified. For example, if${\displaystyle x}$ is an integer variable, to prove that

while${\displaystyle x}$>0do${\displaystyle x}$:=${\displaystyle x}$–1od

refines, or implements the specification${\displaystyle x}$≥0 ⇒${\displaystyle x^{\prime }}$=0, prove

if${\displaystyle x}$>0then${\displaystyle x}$:=${\displaystyle x}$–1; (${\displaystyle x}$≥0 ⇒${\displaystyle x^{\prime }}$=0)else${\displaystyle ok}$fi ⇒ (${\displaystyle x}$≥0 ⇒${\displaystyle x^{\prime }}$=0)

where${\displaystyle ok}$ = (${\displaystyle x^{\prime }}$=${\displaystyle x}$) is the empty, or do-nothing command. There is no need for aloop invariant orleast 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${\displaystyle t}$, and time is measured by counting iterations, then to prove that execution of the previouswhile-loop takes time${\displaystyle x}$ when${\displaystyle x}$ is initially nonnegative, and takes forever when${\displaystyle x}$ is initially negative, prove

if${\displaystyle x}$>0then${\displaystyle x}$:=${\displaystyle x}$–1;${\displaystyle t}$:=${\displaystyle t}$+1; (${\displaystyle x}$≥0 ⇒${\displaystyle t^{\prime }}$=${\displaystyle t}$+${\displaystyle x}$) ∧ (${\displaystyle x}$<0 ⇒${\displaystyle t^{\prime }}$=∞)else${\displaystyle ok}$fi⇒ (${\displaystyle x}$≥0 ⇒${\displaystyle t^{\prime }}$=${\displaystyle t}$+${\displaystyle x}$) ∧ (${\displaystyle x}$<0 ⇒${\displaystyle t^{\prime }}$=∞)

where${\displaystyle ok}$ = (${\displaystyle x^{\prime }}$=${\displaystyle x}$ ∧${\displaystyle t^{\prime }}$=${\displaystyle t}$).

• E.C.R. Hehner,a Practical Theory of Programming, Springer-Verlag 1993. Most recent edition online ata Practical Theory of Programming.

• Publications byEric Hehner.

Thisformal methods-related article is astub. You can help Wikipedia byexpanding it.

• v
• t
• e

• Formal methods
• Formal specification languages
• Logical calculi
• Formal methods stubs

• Articles with short description
• Short description matches Wikidata
• Articles needing additional references from June 2024
• All articles needing additional references
• Articles lacking in-text citations from June 2024
• All articles lacking in-text citations
• All stub articles