Logical Derivation of Computer Programs

The method constitutes a powerful new tool for (a) creating error free programs and (b) showing students a completely rigorous mathematical approach to programming. The logic consists of syntactic, semantics-preserving rewriting rules for the standard constructs of a procedural programming language; namely, assignments, sequencing, branches, loops, and procedure calls. Assignments are used as specifications. Both features permit computer science students and practitioners to relate to the method readily. Program derivations comprise a sequence of procedural derivations starting with (a) given specifications and (b) the procedure calls that arise during programming. Procedural derivations are simply logical proofs created with the rewriting rules of the logic.

The book is written as a textbook for a one-semester course on program derivation. The main prerequisite is a solid discrete math course covering Boolean algebra, propositional calculus via truth tables, and elementary set theory including relations, functions, mathematical induction, the set of natural numbers and finite sequences. lt has been class-tested by the author throughout its development. The book has down-to-earth explanations, lots of details, cogent examples and solved exercises.

Contents: Logical Proofs - Mathematical lnduction - Traditional Programming - A Logic for Procedures - Examples of Program Derivation

About the Author
Dr. Thomas G. Windeknecht is Professor of Engineering and Computer Science at Oakland University, USA. He has released several papers and has previously published 6502 Systems Programming (Little, Brown and Co,. 1983), General Dynamical Processes (Academic Press, 1971), and Color-And-Weave (Van Nostrand Reinhold, 1981), together with M. B. Windeknecht.