The following books by Robert L. Baber are out of print but can be obtained from the sources listed below. An overview of each book is located farther down this page.

1. Software Reflected: the Socially Responsible Programming of Our Computers, North-Holland Publishing Co., Amsterdam, 1982, available in pdf format without charge at SWRefl.pdf. The file is about 62 MB in size. The book is also available from http://www.amazon.com. German translation: Softwarereflexionen: Ideen und Konzepte für die Praxis, Springer-Verlag, Berlin, 1986. Polish translation: O oprogramowaniu inaczej, Wydawnictwa Naukowo-Techniczne, Warszawa, 1989. Overview

2. The Spine of Software: Designing Provably Correct Software - Theory and Practice, John Wiley & Sons, Chichester, 1987, available in pdf format without charge at Spine.pdf. The file is about 70 MB in size. Overview

3. Error Free Software: Know-How and Know-Why of Program Correctness, John Wiley & Sons, Chichester, 1991, available in pdf format without charge at ErrorFreeSW.pdf. The file is about 58 MB in size.The book is also available from the author, see http://www.RLBaber.com for contact addresses. German original: Fehlerfreie Programmierung für den Software-Zauberlehrling, R. Oldenbourg Verlag, München, 1990. Overview

4. Praktische Anwendbarkeit mathematisch rigoroser Methoden zum Sicherstellen der Programmkorrektheit, Walter de Gruyter, Berlin, 1995, available in pdf format without charge at PrakAnw.pdf. The file is about 62 MB in size. The book is also available from the author, see http://www.RLBaber.com for contact addresses. Overview/Übersicht

Some of the above books are also available from "Books on Demand", see http://wwwlib.umi.com/bod.

If you are interested in any of the above books, you might also find my lecture notes for the course "Mathematically Rigorous Software Design" of interest. These lecture notes are available at http://www.cas.mcmaster.ca/~baber/Courses/46L03/MRSDLect.pdf.
 

This book argues that computer programming in its broadest sense (the detailed specification, design and writing of computer software) is by nature an engineering discipline. The fact that it is not generally being treated as such today is a major cause of the many problems that have been and still are being experienced in applying computer systems. The current state of affairs in the “software industry” (especially its ills) and the consequences thereof (both economic and social) are examined. Underlying socioeconomic factors and forces that have lead to the current situation are identified. The most important features of alternative future “software worlds” and the decisions and actions leading to each are described. There are also suggestions for improving the current software situation, as well as discussions on the prerequisites for their implementation.

The arguments presented in this work are unique in the following way: While others seem to concentrate on searching for or developing better technical tools and methods as a solution to the software problems, the author argues that the real cause of today’s software problems is the lack of fundamental knowledge and understanding of informational processes among software practitioners today and NOT the lack of better tools and techniques. The author feels that until this shortcoming is corrected, software quality will remain on a low level.

Contents: Chapters 0. Prologue, The Land of Moc 1. Introduction. 2. The practice of software design and development: yesterday and today. 3. A test for practitioners of the science/art/craft/trade/racket of software design and development. 4. The practice of software design and development: tomorrow? 5. The path from today to tomorrow. Mocpendium: Answers for practitioners of the science/art/craft/trade/racket of software design and development. Bibliography

‘Software engineers and those who would become such’ will find this book’s original approach to the semantics of computer programs of considerable value in their chosen field. The book familiarizes software designers and developers with practically applicable results of research in the theory of proving programs correct. Robert L. Baber’s approach is practical while his mathematical treatment is rigorous. Many examples illustrate the application of the theory to different types of design problems arising in actual practice.

A body of fundamental principles underlying computing science and software engineering has been developed in recent years. These principles provide guidelines for the design process and enable the software engineer to verify systematically and precisely important characteristics of his proposed design, just as, traditionally, engineers have done to achieve reliable, error free designs.

Contents:
Prologue
0 Komputema Simio, the computing monkey of Moc
1 Introduction
Theory
2 Basic semantics of computer programs and programming constructs
3 Proof rules for the individual programming constructs
4 Transfundamental programming constructs
Practice
5 The analysis and verification of programs: methods and examples
6 The construction of correct programs
Epilogue
7 The practice of software engineering tomorrow
Appendices
Bibliography
Index

The pressures of producing good quality software to time and within budget leave little time to explore the theory and potential of formal methods, particularly if the return on time and effort invested seems uncertain.

This concise introduction aims to demonstrate some of the advantages to be gained. The emphasis is on practical applications and immediate usefulness from the design phase onwards. While the techniques described are based on rigorous mathematical foundations the underlying theory is not covered here. The book is designed as a self-study unit with over half its extent devoted to examples and exercises. A bibliography is provided for those motivated to more detailed study.

No free magic wand is offered with this book! The reader will need to spend some time and effort to benefit from the techniques described. Programming experience and a knowledge of basic algebra is assumed.

The book is intended as an initial introduction for the professional software engineer, programmer and student. But, for the programming technician not wishing to study further, this will prove a useful source of practical guidelines and techniques.

Contents: Preface / Mathematical Notation / 0. The Sorcerer’s Apprentices in the Land of the Ret Up Moc / l. Introduction / 2. The Execution of Program Statements: Effects and Assumptions / 3. Foundation for Correctness Proofs / 4. Analysis: Verifying the Correctness of a Program / 5. Designing a Correct Program / 6. Formulating Pre- and Postconditions / 7. Conclusion / Appendix A. Logical (Boolean) Algebra / Appendix B. Solutions to the Exercises / Bibliography / Index / Reference card for applying the proof rules / The most important proof rules

Dem Leserkreis wird eine mathematische Grundlage für die Softwareentwicklung vorgestellt, die den wissenschaftlichen Anforderungen der klassischen Ingenieurwissenschaften entspricht. Neu gegenüber bisher erschienener Literatur über Programmkorrektheit beziehungsweise beträchtlich über bisher in Veröffentlichungen Dargelegtes hinausgehend sind die auf die Belange der Praxis gerichtete Integration ausgewählter theoretischer Kenntnisse, die ausführlichen Untersuchungen über Programmausführungszustände in Korrektheitsbeweisen, die Ausführungen über Rechnerarithmetik, Definitionsbereiche von Programmanweisungen sowie die Systematisierung der praktischen Handhabung.

Aus dem Inhalt: 1. Einleitung / 2. Bisherige Entwicklung auf dem Gebiet der Programmkorrektheitsbeweisführung / 3. Eine praxisgerechte theoretische Grundlage für die Programmkorrektheitsbeweisführung / 4. Bedeutung der Korrektheitsbeweisführung für die ingenieurmäßige Neukonstruktion eines Programms / 5. Bedeutung der Korrektheitsbeweisführung für die Konstruktionsänderung in instabiler Umgebung / 6. Anwendungsaufwand, Voraussetzungen und maschinelle Unterstützung für eine breitere Anwendungsakzeptanz / 7. Spezielle Aspekte der Programmkorrektheitsbeweisführung / 8. Schlußfolgerungen / Anhang 1. Beispiele unterschiedlicher Spezifikationsstufen / Anhang 2. Dokumentationsbeispiel mit Korrektheitsbeweis für den Programmteil “Aufteilen” / Anhang 3. Einige Fehlerschranken für Gleitkommaarithmetik / Anhang 4. Korrektheit eines rekursiven Unterprogramms / Literatur- und Quellenhinweise

Geleitworte
aus dem Buch

Die Qualität technischer Produkte muß gesichert und geprüft sein, bevor sie an einen Kunden ausgeliefert werden. Das gilt auch für Programme!

Bei der Programmentwicklung fehlte lange Zeit ein Ansatz, diese Forderung zu erfüllen. Es wurde drauflos programmiert und geglaubt oder gehofft, daß kein Fehler vorliegt, der die Qualität mindert oder das Programm eigentlich unbrauchbar macht. In der Praxis ist es weitgehend immer noch so. Die in den letzten beiden Jahrzehnten gewonnenen wissenschaftlichen Erkenntnisse zur Qualitätssicherung beim Entwurf und der Implementierung sowie dann auch der stichhaltigen, nachvollziehbaren Überprüfung haben sich kaum bei Praktikern eingeführt; es sei zu mathematisch, zu aufwendig, zu schwierig waren (und sind) häufig gehörte Meinungsäußerungen von Programmierern, Software-Entwicklern und Projektverantwortlichen.

Daß dieses Argument auf schwachen Füßen steht, zeigt diese Schrift. Zu einem ingenieurmäßigen Vorgehen beim Programmentwurf und der Programmierung sind kaum mehr mathematische Kenntnisse als die der Booleschen Algebra und der Mengenlehre erforderlich. Der Aufwand schlägt nicht zu Buche, wenn die Maßnahmen zur Qualitätssicherung beim Entwurf und der Programmierung sogleich mitbehandelt werden; es steigert sich sogar der Dokumentationswert, so daß auch eine qualitätsbezogene Überprüfung fast nebenbei abfällt. Und um Schwierigkeiten zu meistern, ist bekanntermaßen intensive Vorbereitung und stetige Übung der einfachste Weg; man muß es einfach tun, Erfahrung im Umgang mit den Formalien stellt sich ein, plötzlich sind die aufgezeigten Vorgehensweisen ganz selbstverständlich.

Jedem, der sich diesen Herausforderungen bei seiner praktischen Arbeit stellen will, sei diese Schrift zum Studium empfohlen.
Univ.-Prof. Dr.-Ing. Hans-Jürgen Hoffmann
Darmstadt, im Februar 1995

Seit der schrittmachenden Arbeit von Robert Floyd in den 60er Jahren sind uns die Grundideen der Methoden zum Sicherstellen der Korrektheit von sequentiellen Computerprogrammen bekannt. Mit den Ergänzungen von (u.a.) Mills, Majster-Cederbaum und de Bruijn haben wir allgemein anwendbare theoretische Grundlagen für dieses Gebiet gewonnen. Heute gibt es keinen theoretischen Grund, die Korrektheit von Programmen, die in der Praxis geschrieben werden, nicht zu beweisen. Trotz diesen erfreulichen Tatsachen muß festgestellt werden, daß diese Ideen in der Industrie sehr selten angewendet werden. Es stellt sich die Frage, “Warum hat sich die Anwendung von mathematischen Methoden im Bereich Software Engineering nicht weiter durchgesetzt?”

Meines Erachtens liegt das Hauptproblem in den bisher erarbeiteten Antworten auf die zwei Darstellungsfragen:

In dieser Arbeit von Robert Baber bekommen die Leser und Leserinnen praktische Vorschläge und Beispiele, die die Lücke zwischen Theorie und Praxis überbrücken. Es wird gezeigt, wie man die seit 20 Jahren bekannte theoretische Grundlage in einem praktikablen Verfahren anwenden kann.

In der vorliegenden Arbeit findet man Datenzustandsdarstellungen ohne die Einschränkung, die in den Ansätzen von Floyd, Hoare und Dijkstra impliziert sind. Man findet auch neue Vorschläge zur Beschreibung von Funktionen und Prädikaten. Viele Ingenieure werden die hier eingeführte Notation verständlicher als die klassische Schreibweise finden.

Dieses Buch baut auf viele frühere Arbeiten auf und faßt die verschiedenen Ansätze zusammen. Es wird allen in der Praxis beschäftigten Ingenieuren und Informatikern empfohlen. Das umfangreiche Literaturverzeichnis wird auch vielen Forschern behilflich sein.
Prof. Dr. rer. nat. (h.c.) David Lorge Parnas, Ph.D., FRSC
Department of Electrical and Computer Engineering
McMaster University
Hamilton, Ontario, Canada L8S 4K1