Books by
Robert Laurence Baber
2012 August 4

Information on my latest book, The Language of Mathematics: Utilizing Math in Practice (John Wiley & Sons, Inc., 2011), is available at A general overview of my books, including plans for the future, is available at

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 35 MB in size. 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 25 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 10 MB in size. The book is also available from the author, see for contact addresses. The German original, Fehlerfreie Programmierung für den Software-Zauberlehrling, R. Oldenbourg Verlag, München, 1990, is available in pdf format without charge at SwZaub.pdf. The file is about 6 MB in size. 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 20 MB in size. The book is also available from the author, see for contact addresses. Overview/Übersicht

If you are interested in any of the above books, you might also find

Software Reflected: The Socially Responsible Programming of Our Computers
Overview from the publisher’s fly sheet

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

The Spine of Software: Designing Provably Correct Software — Theory and Practice
Overview from the publisher’s fly sheet

‘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.

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

Error-free Software: Know-how and Know-why of Program Correctness
Overview from the publisher’s fly sheet

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

Praktische Anwendbarkeit mathematisch rigoroser Methoden zum Sicherstellen der Programmkorrektheit
Übersicht aus dem Flugblatt des Verlags

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

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:

  • Wie können wir die durch Programme verwirklichten Funktionen leserlich beschreiben?
  • Wie können wir Datenzustande beschreiben?

  • In den weit verbreiteten Arbeiten von Floyd, Hoare und Dijkstra wird angenommen, daß eine 1:1 Beziehung zwischen Bezeichnern und Programmvariablen besteht. Diese Annahme ermöglicht eine einfache Beschreibung der Datenzustande. Leider trifft diese Annahme bei den meisten in der Praxis benutzten Programmiersprachen nicht zu. Die Ansätze von Mills, Majster-Cederbaum, de Bruijn und anderen sind allgemeingültig, weil in diesen Arbeiten einfach von “states” gesprochen wird, ohne eine bestimmte Zustandsdarstellungsweise anzunehmen. Dies hat zur Folge, daß der Ingenieur, der diese Methoden anwenden will, seine eigene Darstellungsweise erfinden muß. Es hat sich herausgestellt, daß dies für die Mehrheit der Praktiker zu schwierig ist und daß sie deswegen auf die formale Überprüfung von Programmkorrektheit verzichten.

    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