Dijkstra-Scholten Predicate Calculus: Concepts and Misconceptions

The paper focusses on the logical backgrounds of the Dijkstra-Scholten program development style for correct programs. For proving the correctness of a program (i.e. the fact that the program satisfies its specifications), one often uses a special form of predicate calculus in this style of programming. We call this the Dijkstra-Scholten (DS) predicate calculus, since [DS90] is the first place in which it is described. DS predicate calculus can be conceived of as a logically sound and complete manipulation technique for dealing with logical formulas which also contain programming variables. We relate DS predicate calculus to the classical logical formalism, by contrasting its syntax, derivation rules and semantics to the classical framework. We also comment on ractions of DS predicate calculus: the set-theoretical and the algebraic approach. so, we give DS predicate calculus and its abstract variants a firm basis, on a par with the foundations of the well-known first order logic....

• Type: Journal
• Year: 1998
• Where: ACTA
• Authors: Lex Bijlsma, Rob Nederpelt
• Keywords: ACTA 1998, Calculus, Classical Logical Formalism, Program Development Style