Predicative programming Part I
Eric C. R. Hehner · Communications of the ACM · 1984
Programs are given a new semantics with the merit that a specification written as a first-order predicate can be refined, step by step, to a program via the rules of Predicate Calculus. The semantics allows a free mixture of predicate and programming notations, and manipulation of programs.