Reasoned Programming by Krysia Broda, Susan Eisenbach, Hessam Khoshnevisan, and, Steve Vickers.
From the preface:
How do you describe what a computer program does without getting bogged down in how it does it? If the program hasn’t been written yet we can ask the same question using a different tense and slightly different wording: How do you specify what a program should do without determining exactly how it should do it? Then we can add the question: When the program is written, how do you judge that it satisfi es its specifi cation?
In civil engineering, one can ask a very similar pair of questions: How can you specify what a bridge should do without determining its design? And, when it has been designed, how can you judge whether it does indeed do what it should?
This book is about these questions for software engineering, and its answers can usefully be compared with what happens in civil engineering. First, a speci fication is a different kind of thing from a design; the specifi cation of a bridge may talk about loadbearing capacity, deflection under high winds and resistance of piers to water erosion, while the design talks about quite different things such as structural components and their assembly. For software, too, speci fications talk about external matters and programs talk about internal matters.
The second of the two questions is about judging that one thing satisfi es another. The main message of the book and a vitally important one is that judgement relies upon understanding. This is obviously true in the case of the bridge; the judgement that the bridge can bear the speci fied load rests on structural properties of components enshrined in engineering principles, which
in turn rest upon the science of materials. Thus the judgement rests upon a tower of understanding.This tower is well-established for the older engineering disciplines; for software engineering it is still being built. (We may call it software science.’) The authors have undertaken to tell students in their fi rst or second year about the tower as it now stands, rather than dictate principles to them. This is refreshing in software engineering there has been a tendency to substitute formality for understanding. Since a program is written in a very formal language and the specifi cation is also often written in formal logical terms, it is natural to emphasize formality in making the judgement that one satifis es the other. But in teaching it is stultifying to formalize before understanding, and software science is no exception — even if the industrial signi ficance of a formal veri fication is increasingly being recognized.
This book is therefore very approachable. It makes the interplay between speci fication and programming into a human and flexible one, albeit guided by rigour. After a gentle introduction, it treats three or four good-sized examples, big enough to give con fidence that the approach will scale up to industrial software; at the same time, there is a spirit of scienti c enquiry. The authors have made the book self-contained by including an introduction to logic written in the same spirit. They have tempered their care for accuracy with a light style of writing and an enthusiasm which I believe will endear the book to students.
Apologies for the long quote but I like the style of the preface. 😉
As you may guess from the date, 1994, the authors focus on functional programming, Miranda, and Modula-2.
Great read and highly recommended.
I first saw this in a tweet by Computer Science.