Books

Short works

Books : reviews

Carroll Morgan.
Programming from Specifications.
Prentice Hall. 1990

(read but not reviewed)

Building on recent advances in software engineering, this book teaches programming as the step-by-step development of specifications into code. The method produces correct programs and their development histories, creating a record of design decisions that simplifies program maintenance.

The specifications are based on ordinary logic, and resemble Z and VDM. The laws of program development are clearly explained, and are illustrated with examples, case studies, exercises and answers.

The resulting programs are easily cast in conventional languages like Pascal. Recursion, modularity and data refinement are included.

Programming from Specifications is intended for both students and experienced programmers.

Carroll Morgan, Trevor Vickers.
On the Refinement Calculus.
Springer. 1992

On the Refinement Calculus collects together the work accomplished at Oxford on the refinement calculus: the rigorous development, from state-based assertional specifications, of executable imperative code.

The refinement calculus is a notation and set of rules for deriving imperative programs from their specifications. It is distinguished from earlier methods (though based on them) because the derivations are carried out within a single ‘programming’ language: there is no separate language of specifications. So far, it has uncovered ‘miracles’, novel techniques of data refinement, a simpler treatment of procedures, ‘conjunction’ of programs, and a lightweight treatment of types in simple imperative programs.

The integration of specifications and code was proposed by R.-J. R. Back in the late 1970’s, when he inserted specifications into Dijkstra’s language based on weakest preconditions. At Oxford, this same idea, although much later, was amplified both by the strong research tradition in specification and by the challenge offered by the University’s new undergraduate degree course in computer science.

On the Refinement Calculus gives one view of the development of the refinement calculus and its attempt to bring together – among other thinqs – Z specifications and Dijkstra’s programming language. It is an excellent source of reference material for all those seeking the background and mathematical underpinnings of the refinement calculus.

Annabelle McIver, Carroll Morgan, eds.
Programming Methodology.
Springer. 2003

Important advances in the principles for design, construction, and organization of computer programs have enabled software to keep pace with the remarkable advances in computing speed and memory. In addition to allowing for an all-pervasive computing technology, these key methods are beginning to feed back on, and influence, hardware design.

Programming Methodology is a comprehensive edited volume that concentrates on new and emerging techniques for constructing modern applications, while also addressing the problems software designers face as they attempt to develop highly complex applications that actually work. Contributions to the book are from leading academics and industrialists of the International Federation for Information Processing’s Working Group 2.3, whose mission is to assess methodologies for creating and improving the quality of software and systems. The work is thematically organized into three sections: models and correctness; programming techniques; and applications and automated theories.

Topics and Features:

• Proposes practical solutions—and their theoretical foundations—to current software and systems challenges

• Incorporates examples from a wide range of applications, such as security, telephony, and circuit design

• Examines challenges to systems engineering, automating theories, and the robust design of concurrent systems

• Highlights recent technical advances in the ways that software systems are designed and verified

• Provides concise and helpful introductions to each carefully organized subsection of related material

This state-of-the-art survey on key new foundational topics in programming methodology is an essential resource developed by leading international computer scientists, programmers, and software systems designers. It offers an authoritative reference and guide to modern software theory and practice for programmers, developers, computer scientists, and software engineers.

The chapters are collected into three parts: • Models and correctness • Programming techniques • Applications and automated theories

Contents

Cliff B. Jones. Wanted: a compositional approach to concurrency. 2003
Ralph-Johan Back, Joakim von Wright. Enforcing behaviour with contracts. 2003
Ernie Cohen. Asynchronous progress. 2003
Jayadev Misra. A reduction theorem for concurrent object-oriented programs. 2003
Manfred Broy. Abstractions from time. 2003
Ian J. Hayes. A predicative semantics for real-time refinement. 2003
Michael Jackson. Aspects of system description. 2003
Peter Henderson. Modelling architectures for dynamic systems. 2003
Dines Bjorner. "What is a method?" -- an essay on some aspects of domain engineering. 2003
Manfred Broy. Object-oriented programming and software development -- a critical assessment. 2003
C. A. R. Hoare, He Jifeng. A trace model for pointers and objects. 2003
Daniel Jackson. Object models as heap invariants. 2003
K. Rustan M. Leino, Greg Nelson. Abstraction dependencies. 2003
Benjamin C. Pierce. Type systems. 2003
John C. Reynolds. What do types mean? -- from intrinsic to extrinsic semantics. 2003
Natarajan Shankar. Automated verification using deduction, exploration, and abstraction. 2003
Pamela Zave. An experiment in feature engineering. 2003
Eric C. R. Hehner, Theodore S. Norvell, Richard F. Paige. High-level circuit design. 2003
Suresh Chari, Charanjit S. Jutla, Josyula R. Rao, Pankaj Rohatgi. Power analysis: attacks and countermeasures. 2003
A probabilistic approach to information hiding. 2003