Hehner E.C.R. a Practical Theory of Programming

Toronto: University of Toronto, 2019. — 250 p.The subject of this book sometimes goes by the name “programming methodology”, “science of programming”, “logic of programming”, “theory of programming”, “formal methods of program development”, or “verification”. It concerns those aspects of programming that are amenable to mathematical proof. A good theory helps us to write precise specifications, and to design programs whose executions provably satisfy the specifications. We will be considering the state of a computation, the time of a computation, the memory space required by a computation, and the interactions with a computation. There are other important aspects of software design and production that are not touched by this book: the management of people, the user interface, documentation, and testing. In the first usable theory of programming, often called “Hoare's Logic”, a specification is a pair of predicates: a precondition and postcondition (these and all technical terms will be defined in due course). A closely related theory uses Dijkstra's weakest precondition predicate transformer, which is a function from programs and postconditions to preconditions, further advanced in Back's Refinement Calculus. Jones's Vienna Development Method has been used to advantage in some industries; in it, a specification is a pair of predicates (as in Hoare's Logic), but the second predicate is a relation. There are theories that specialize in real-time programming, some in probabilistic programming, some in interactive programming. The theory in this book is simpler than any of those just mentioned. In it, a specification is just a binary expression. Refinement is just ordinary implication. This theory is also more comprehensive than those just mentioned, applying to both terminating and nonterminating computation, to both sequential and parallel computation, to both stand-alone and interactive computation. All at the same time, we can have variables whose initial and final values are all that is of interest, variables whose values are continuously of interest, variables whose values are known only probabilistically, and variables that account for time and space. They all fit together in one theory whose basis is the standard scientific practice of writing a specification as a binary expression whose (nonlocal) variables represent whatever is considered to be of interest. The emphasis throughout this book is on program development with proof at each step, rather than on proof after development.Basic Theories.
Basic Data Structures.
Functions.
Specifications.
Programming Language.
Recursive Data Definition.
Theory Design and Implementation.
Concurrency,
Interaction.
Exercises.