Carroll Morgan

Programming from Specifications

Second Edition

© Carroll Morgan 1990, 1994 and 1998.

Permission is granted to copy this material for private study; for other uses please contact the author.

About this web edition

Programming from Specifications presents a rigorous treatment of most elementary program-development constructs, including iteration, recursion, procedures, parameters, modules and data refinement.

The second edition retains the simple approach of the original: the integration of specification, development and coding, and the use of ordinary (classical) logic. Additions include more material on data refinement, a complete chapter on recursively defined types, and two further extended case studies.

About the first edition

In the growing list of programming methodology texts, Programming from Specifications is currently the best.
Science of Computer Programming

Influential [or] even seminal... I regard it as one of the most significant and thoughtful formal methods works published in the last ten years.

Overall, it is difficult to exaggerate the importance of this book, which breaks quite new ground in the way formal manipulation of specifications is presented...

Differences from the first edition
1.  Programs and refinement
2.  The predicate calculus
3.  Assignments and sequential composition
4.  Alternation
5.  Iteration
6.  Types and declarations
7.  Case study: Square root
8.  Initial variables
9.  Constructed types
10.  Case study: Insertion Sort
11.  Procedures and parameters
12.  Case study: Heap sort
13.  Recursive procedures
14.  Case study: The Gray code
15.  Recursive types
16.  Modules and encapsulation
17.  State transformation and data refinement
18.  Case study: Majority voting
19.  Origins and conclusions
20.  Case study: A paragraph problem
21.  Case study: The largest rectangle under a histogram
22.  Case study: A mail system
23.  Semantics
A.  Some laws for predicate calculation
B.  Answers to some exercises
C.  Summary of laws
Answers to all exercises (contact the author)
The whole text (500K)
Back to the top.

Look here, here or here for other formal methods material.