Thinking Programs Logical Modeling and Reasoning About Languages, Data, Computations, and Executions, 2nd ed. (Wolfgang Schreiner) (z-library.sk, 1lib.sk, z-lib.sk)

Texts & Monographs in Symbolic Computation Wolfgang Schreiner Thinking Programs Logical Modeling and Reasoning About Languages, Data, Computations, and Executions Second Edition

Texts & Monographs in Symbolic Computation A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria Series Editor Peter Paule, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria

Mathematics is a key technology in modern society. Symbolic Computation is on its way to become a key technology in mathematics. “Texts and Monographs in Symbolic Computation” provides a platform devoted to reflect this evolution. In addition to reporting on developments in the field, the focus of the series also includes applications of computer algebra and symbolic methods in other subfields of mathematics and computer science, and, in particular, in the natural sciences. To provide a flexible frame, the series is open to texts of various kind, ranging from research compendia to textbooks for courses. Indexed by zbMATH.

Wolfgang Schreiner Thinking Programs Logical Modeling and Reasoning About Languages, Data, Computations, and Executions Second Edition

Wolfgang Schreiner RISC Johannes Kepler University Linz, Austria ISSN 0943-853X ISSN 2197-8409 (electronic) ISBN 978-3-031-99704-4 ISBN 978-3-031-99705-1 (eBook) Texts & Monographs in Symbolic Computation https://doi.org/10.1007/978-3-031-99705-1 © The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG 2021, 2026 This work is subject to copyright. All rights are solely and exclusively licensed by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. This Springer imprint is published by the registered company Springer Nature Switzerland AG The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland If disposing of this product, please recycle the paper.

Meinen Eltern

Foreword to the First Edition When I started my study of mathematics at the University of Innsbruck in 1960, like most freshmen, I was intimidated and impressed by the apparent intelligence of the professors who gave proofs of abstract knowledge, which was far from the concrete thinking about mathematical objects which we had seen in high-school. However, after some time, in secret, I started to doubt the quality of some of the hand-waving proofs and I wanted to look behind the scene. For this, in parallel and independent of the curriculum, I started to dig through the books on logic I found in the general library of the university. (For some reason, most of them had a yellow cover — the “Springer Books on Logic”. Subconsciously, this may have been the reason why, many years later, I decided that the cover the Journal of Symbolic Computation should be yellow, when I founded it in 1985.) From that time on, it became more and more clear to me that logic is the essence of mathematical thinking and, luckily, very soon after my start as a mathematics student I got the chance to become one of the first programmers on the first computer at our university and the computer appeared to me as “materialized logic”. Since then, for me, mathematics, logic, and computer science was just one field and I am still fascinated and convinced by the repeated algorithmic cycles through object and meta-levels to reach higher and higher states of insight and a more and more efficient grasp of the thinking process. Understanding the spiral of logic for (algorithmic) mathematics and algorithmic mathematics for logic is so important also for steering a clear course in a time of frequent new and fancy catch words that may suggest that logical clarity and brilliance is not any more relevant in a time of “intelligent machines”. In 1979, in contrast to the usual analysis/linear algebra approach, I dared to give an introduction to mathematics for first semester computer science students which was nothing else than a practical introduction to predicate logic as a working language and a unified frame for proving and programming. Over the years, many of my students shared this view on the fundamental theoretical and practical importance of logic for mathematics and informatics and did remarkable work developing ideas and tools for supporting this kind of thinking. Wolfgang Schreiner embarked on this type of research, teaching, and software development already in the mid-nineties and, over vii

viii Foreword to the First Edition the years, accumulated enormous know-how and produced impressive and extensive teaching material and software tools for the theoretical foundation and the practical application of logic in mathematics and computer science, notably in mathematics and computer science teaching. Now, he presents this enormous amount of work in a coherent book. I think there is hardly any other book that combines the foundation of logic, the applications of logic in computer science, and software for logic in an equally rich and comprehensive way. I wish the book a wide distribution. Given the outstanding didactic qualification of Wolfgang Schreiner, I am sure that the book will be extremely helpful for students of mathematics and computer science to get a profound training of the thinking technology that is in the center of the present age and will stay and become even more important in the next turns of the spiral of innovation. It is also a special pleasure for me that the book appears in the RISC book series on symbolic computation with the Springer Verlag whose “yellow books” lured me into the field of (algorithmic) logic so many years ago. When I founded the RISC book series in 1993, for some reason, we decided that the cover should be grey. However, the contents of the books in this series were very much “yellow” all the time. It is great to see that, since Peter Paule took over the editorship and is giving enormous drive to the series, yellow is taking over also on the covers. Hagenberg, March 2021 Bruno Buchberger

Preface to the Second Edition It is a great privilege for an author to be offered the opportunity to revise a book that was conceptualized more than a decade ago and subsequently elaborated in a period of more than five years. However, it also poses the obligation to seriously consider some basic questions, among them most important: Is the core topic still relevant? Are the fundamental ideas still sound? Is the organization still adequate? Should old material be dropped and/or new material be added? As for the core topic and the fundamental ideas: I am personally convinced as ever that the question of clear thinking about programs is as relevant as ever. This is also and in particular true in a time when more and more computer code is automatically generated by tools that are claimed to embed “artificial intelligence”. However, at their core, these tools rely on statistical principles that cannot provide hard correctness guarantees: often the results seem alright, but sometimes they contain subtle errors; in the worst case, they are complete blunder. It is ultimately still up to us human beings as embodiments of “natural intelligence” to evaluate an automatically generated solution, judge its adequacy, and unveil its problems. Thus we have to be able to think about programs, within a suitable mental framework based on a language that is adequate to express our thoughts. The language of logic still seems the primary tool for this purpose. As for the organization and the material: The second part of the book has been carefully designed to elaborate in the language of logic a sequence of tightly integrated other formal languages, starting with a language of specifying abstract datatypes, proceeding to a language of describing sequential programs, and culminating in a language for modeling concurrent systems, along with the methods needed for giving these languages a precise semantics and for reasoning about the artifacts described in these languages. For this purpose, the first part of the book presents the necessary foundations, in particular logic, set theory, and recursion theory; to these foundations the second part continuously refers. Even if some of the foundational material may be skipped on first reading, it is ultimately the basis for understanding the finer points of the later language formalizations; thus I refrained from putting the axe to any part of it. On the other side, considering the volume of the material already present, I (mostly) shied away from adding even more; any benefit of going into more depth ix

Preface to the Second Editionx in some aspects of the presentation would be counterbalanced by the detriment of losing the focus on the main messages that the book tries to convey. Ultimately, I decided to mostly concentrate in this new edition on improving not the extent but the quality of the presentation. Fortunately, having used a significant portion of the book in multiple iterations of my own courses, much of its content has been validated by repeated inspection, presentation, and discussion. However, by this process also multiple deficiencies have come to light, most of a minor nature, but also a few with larger significance; also re-reading the whole book from front to back with a fresh mind has helped to reveal some shortcomings. This second edition amends the deficits of the first one and thus represents a considerable advancement. Furthermore, while I refrained from adding to the core material (which, by its mathematical/logical nature, should essentially represent “eternal truths”), I’ve updated several of the (more time dependent) “software appendices” at the end of each chapter to take recent developments into account. In particular, I’ve added presentations of new software respectively of new features of software that was already discussed in the first edition. So, all in all, this second (2025) edition differs from the first (2021) one in the following main points: • Typesetting and typography have been improved in numerous places; several editing mistakes (in particular broken references across chapters) have been corrected. Also various omissions, inaccuracies, and errors have been remedied, both in the formal content and in the natural language text. All in all, almost every third page of the first edition has been modified in some way or other. • In Appendix “Abstract Syntax Trees in OCaml and SLANG” of Chapter 1 and in Appendix “Language Semantics in OCaml, the K Framework, and SLANG” of Chapter 7, I describe the application of a new software tool, the “semantics-based language generator” SLANG, to develop rapid prototype implementations of languages from their formal definitions. • In Appendix “Program Reasoning in RISCAL and the RISC ProgramExplorer” of Chapter 8 and in Appendix “System Analysis in TLA+ and RISCAL” of Chapter 9, I outline new capabilities of the RISCAL model checker: first, proof- based reasoning via the new RISCTP interface to several automated theorem provers; second, model checking system properties expressed in the language of linear temporal logic (LTL) via a new internal LTL model checker. The added material amounts to about 25 new pages in the second edition. The literature references and the web page accompanying the book have been correspondingly updated as well. I am thankful to all the students who helped me to reflect on and improve the material for this second edition; any (old or new) errors, however, are still my own. Hagenberg, April 2025 Wolfgang Schreiner

Revised Preface to the First Edition Motivation The purpose of this book is to outline some basic principles that enable developers of computer programs (computer scientists, software engineers, programmers) to more clearly think about the artifacts they deal with in their daily work: data types, programming languages, programs written in these languages that compute from given inputs wanted outputs, and programs for continuously executing systems. In practice, thinking about these artifacts is often muddled by not having a suitable mental framework at hand, i.e., a language to appropriately express this thinking. The core message that we want to convey is that clear thinking about programs can be expressed in a single “universal” language, the formal language of “logic”. In particular, with the help of logic we can achieve the following goals: • Modeling: we can unambiguously describe the meaning of syntactic entities such as the behavior of computer programs. • Specifying: we can precisely formulate constraints we impose on (the meaning of) these entities such as requirements on program executions. • Reasoning: we can rigorously show that the entities indeed satisfy these constraints, e.g., that programs satisfy their specifications. However, in order to enable this clear thinking about computer programs, we also need a framework to relate the syntactic artifacts (that have a priori not any content beyond their structure) to their formal meaning (characterized by logical formulas). The description of this relationship can be generally based on three principles: • A grammar that describes the basic structure of syntactic phrases. • A type system that further restricts the phrases to certain “well-formed” ones. • A function that maps every well-formed phrase to its meaning. Thus we can give arbitrary syntactic phrases a precise meaning about which we can rigorously reason. In fact, we will use this approach of denotational semantics uniformly throughout this book in order to define various formal languages, starting with the language of logic itself and ending with a language of concurrent systems. xi

xii Revised Preface to the First Edition Throughout most of this book, we understand by “logic” the classical first-order variant of predicate logic, short first-order logic, the “lingua franca” of formal modeling and reasoning today. While some aspects of computer programming may practically profit from more general frameworks such as “higher-order logic” or “temporal logic” (which we will also discuss in this book), first-order logic is conceptually sufficient for most purposes and in any case provides a solid basis for understanding all kinds of logical extensions. Apart from its universal elegance and expressiveness, our “logical” approach to the formal modeling of and reasoning about computer programs has another advantage: due to advances in computational logic (automated theorem proving, satisfiability solving, model checking), nowadays much of this process can be supported by software. This book therefore accompanies its theoretical elaborations by practical demonstrations of various systems and tools that are based on respectively make use of the logical underpinnings. We hope that this will convincingly demonstrate also the actual usefulness of the presented approach. This book has been written with a broad target audience in mind that encompasses students and practitioners in computer science and computer mathematics; it therefore tries to be as self-contained as possible and not assume a particular background in logic or mathematics. However, it focuses on a “logical” perspective to the overall areas of “formal methods” and “formal semantics” which in several aspects differs from other presentations of this topic. To get a more comprehensive picture (especially on alternative approaches), the reader might want to consult additional resources; the book gives various recommendations for further reading. Content To introduce the basic themes of this book and demonstrate their ultimate purpose, an introductory section “Logic for Programming: A Perspective” gives a short historical account on the development of logical modeling and reasoning about computer programs and presents examples of practical applications of these techniques in industrial software development today. The main contents of this book are then organized in two parts: Part I: The Foundations This part introduces the basic language of logic and math- ematics that is used throughout the remainder of the book. While an impatient reader (such as the author himself!) may be inclined to skip over this part, we advise to study at first reading at least Chapter 1 “Syntax and Semantics” which introduces the themes that are fundamental to this book: • context-free grammars (inductive definitions of formal languages as sets of phrases represented by abstract syntax trees), • type systems (logical inference systems which restrict these languages to certain “well-formed” phrases), • semantics functions (inductively defined functions which give these phrases a meaning by mapping them to mathematical objects), and

• the accompanying principle of structural (more general: rule) induction which enables us to reason about these constructions. Revised Preface to the First Edition xiii The subsequent chapters elaborate these concepts in more detail (the impatient reader may skip over them at first reading and consult them later on demand). Chapter 2 “The Language of Logic” applies above principles to introduce the syntax and semantics of first-order logic, the core language of this book. Chapter 3 “The Art of Reasoning” continues this presentation by introducing the concept of logical proof and by introducing a variant of the sequent calculus as a formal framework for proof construction. Chapter 4 “Building Models” describes how with the language of logic models of reality (theories and data types) can be constructed in which we subsequently operate. Chapter 5 “Recursion” discusses the semantics of various forms of recursion, including inductive and coinductive definitions of functions and relations, using a restricted variant of fixed point theory. The material presented in these chapters (and much more) can be similarly found in various texts on logic and mathematics for computer science, however with non-uniform notions and notations; our goal here is to give a minimal consistent framework as a sufficient and necessary basis of Part II of this book. Part II: The Higher Planes This part contains the actual core contents of the book: • Chapter 6 “Abstract Data Types” discusses the formal specification of abstract data types by logical axioms that the operations on the types must satisfy; the types may consist of finite values characterized by their constructor operations but also of potentially infinite values characterized by their observer operations. For this purpose, we gradually introduce a formal type specification language with a static type system and give it a semantics as models of first-order formulas; these models may be restricted to a particular class of candidates by special kinds of specifications (generated/free, cogenerated/cofree). We also discuss specifying in the large by various principles to compose smaller specifications to bigger ones. The chapter does not only describe the modeling of types but also the basic techniques for reasoning about them; it also discusses the refinement of more abstract types to more concrete ones. • Chapter 7 “Programming Languages” discusses the formal semantics of pro- gramming languages. For this we extend the previously introduced type speci- fication language to an imperative (command-based) programming language whose semantics we describe by two approaches. In denotational semantics, we first map commands to partial functions on program states; these functions are defined by logical terms. Later we generalize this classical “functional” style to a non-classical but much more flexible “relational” style where commands are mapped to state relations defined by logical formulas. In operational semantics, we give programs a semantics by mapping them to transition relations defined by logical inference systems; we then show the essential equivalence of deno- tational and operational semantics. We apply these techniques to model the translation of the command language to a low-level machine language and prove the correctness of the translation. Finally, we extend the command language by the abstraction mechanism of procedures and model their semantics.

• Chapter 8 “Computer Programs” discusses the formal verification of programs by various closely related calculi; the chapter thus lifts the level of reasoning from the previously discussed layer of programming languages to that of programs written in these languages. After discussing the formal specification of computational problems as the basis of program verification, we present the Hoare calculus and prove its soundness with respect to the semantics of the language. We continue with Dijkstra’s predicate transformer calculus that maps commands to functions on formulas over states; further on we complement this approach by presenting a relational calculus that maps programs to formulas over state pairs. A good part of the chapter is dedicated to the pragmatics of verifying the partial correctness and termination of programs, which requires the human to devise adequate loop invariants and termination measures; here we give several concrete verification examples. Finally we discuss the abstract concept of command refinement from which we derive the concrete principles of modular reasoning about the correctness of procedure-based programs. • Chapter 9 “Concurrent Systems” discusses the formal modeling of and reason- ing about systems exhibiting nondeterministic behavior (concurrent/reactive systems). For this we extend the previously introduced command language to a language of shared systems where concurrent activities interact via a common state as well as to a language of distributed systems whose components interact by exchanging messages. We give these languages a semantics by mapping them to labeled transition systems; these are described by logical formulas that denote initial state conditions and transition relations. For specifying properties of such systems we extend first-order logic to linear temporal logic whose formulas are interpreted over system runs. The proof-based verification of such properties requires the human to devise adequate system invariants; we discuss the verification of such invariants expressing safety properties of the system and also the verification of a particular class of liveness properties which ensure the progress of the system execution. Finally we investigate the refinement of more abstract systems (models) to more concrete systems (implementations). xiv Revised Preface to the First Edition Altogether these chapters thus present the syntax and semantics of a language that encompasses abstract type declarations, imperative programs whose behaviors are specified by formulas in first-order logic, and concurrent systems whose behaviors are specified in linear temporal logic; they discuss corresponding calculi for the verification of the programs with respect to specifications and for the refinement of more abstract programs to more concrete ones. Software Each chapter is accompanied by a section that illustrates the practical relevance of the presented theoretical material by some software system or programming language that is based on the presented concepts respectively makes use of them: • The functional programming language OCaml.

Revised Preface to the First Edition xv 1 Syntax and Semantics 2 The Language of Logic 3 The Art of Reasoning 4 Building Models 5 Recursion 6 Abstract Data Types 7 Programming Languages 8 Computer Programs 9 Concurrent Sytems Fig. 0.1 Chapter Dependencies • The semantics-based language generator SLANG. • The proof assistant RISC ProofNavigator. • The interactive theorem prover Isabelle/HOL. • The algebraic specification language CafeOBJ. • The common algebraic specification language CASL. • The executable semantics framework K. • The algorithm language and model checker RISCAL. • Logic, Formal Modeling: chapters 1–3. • Set Theory, Fixed Point Theory: chapters 4–5. • Formal Specification of Abstract Data Types: chapter 6. The program verification environment RISC ProgramExplorer. • • The TLA+ toolbox for modeling and checking concurrent systems. Most of these tools have been developed by other researchers; SLANG, the RISC ProofNavigator, the RISC ProgramExplorer, and RISCAL are the results of the author’s own work. All the presented software is freely available; the reader may download the examples presented in each section (see below) and run them on their own. Teaching and Further Study While of course the various chapters of this book in general linearly depend on each other in that each chapter may refer to some material presented earlier, Figure 0.1 tries to outline the main dependencies by solid arrows (the dotted arrows represent weak dependencies); their consideration may be indeed useful in selecting material from this book for university courses that teach some specific topics such as: • Formal Semantics of Programming Languages: chapter 7 (with elements of ch. 5).

• Formal Methods in Software Development: chapter 8. • Formal Models of Parallel and Distributed Systems: chapter 9. xvi Revised Preface to the First Edition Indeed the author has taught courses (respectively participated in teaching) on most of these topics using material from this book (partially complemented by other more in-depth material). In fact, since this book presents an integrated view on various (related but not identical) subjects, we had to choose from each field those aspects that we considered essential for conveying our core message: how by some universal principles of logical modeling and reasoning a software developer can better understand the artifacts that he/she is dealing with. This necessarily comes at the price that many other (also important) elements had to be neglected. To partially compensate for these gaps, each chapter concludes with a section “Further Reading” that suggests specific literature (mainly textbooks) that cover the presented topic in more depth or breadth, but typically from a different perspective. Lecturers, students, and readers may complement our presentation by additional material from these references. Web Page and Exercises This book is accompanied by electronic material available from the following URL: https://www.risc.jku.at/people/schreine/TP In particular, this web page contains all software examples presented in this book and exercises for the topics of the various book chapters. Acknowledgments The author has written this book as an associate professor at the Research Institute of Symbolic Computation (RISC), a stimulating Austrian institution for research, education, and application of algebraic and logic methods founded by Bruno Buch- berger, formerly directed by Franz Winkler, and currently directed by Peter Paule; RISC is located in the Softwarepark Hagenberg and organizationally part of the Johannes Kepler University Linz. The book is based on the author’s experience in teaching corresponding courses at this university, feedback received from students, and discussions with colleagues. In particular, Patrick Riegler has helped to improve the chapters of Part II of this book; Chapters 2 “The Language of Logic” and 3 “The Art of Reasoning” have been influenced by the course module “First-Order Logic” jointly taught by the author and Wolfgang Windsteiger. We are also grateful to the anonymous reviewers whose suggestions helped to improve the manuscript (in particular by adding the introductory section with examples of industrial applications of formal methods). All errors, however, are the author’s own. Hagenberg, March 2021 Wolfgang Schreiner

Contents Logic for Programming: A Perspective . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Part I The Foundations 1 Syntax and Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.1 Abstract Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.2 Structural Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 1.4 Type Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 1.5 The Semantics of Typed Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Abstract Syntax Trees in OCaml and SLANG . . . . . . . . . . . . . . . . . . . . . 33 2 The Language of Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 2.1 First-Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 2.2 Informal Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 2.3 Well-Formed Terms and Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 2.4 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 2.5 Free and Bound Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 2.6 Formal Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 2.7 Validity, Logical Consequence, and Logical Equivalence . . . . . . . . . . 67 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 The Logic of the RISC ProofNavigator . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 xvii

xviii Contents 3 The Art of Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 3.1 Reasoning and Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 3.2 Inference Rules and Proof Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 3.3 Reasoning in First Order Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 3.4 Reasoning by Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Reasoning with the RISC ProofNavigator . . . . . . . . . . . . . . . . . . . . . . . . . 109 4 Building Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 4.1 Axioms and Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 4.2 The Theory of Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 4.3 Products and Sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 4.4 Set-Theoretic Functions and Relations . . . . . . . . . . . . . . . . . . . . . . . . . 130 4.5 More Type Constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137 4.6 Implicit Definitions and Function Specifications . . . . . . . . . . . . . . . . . 140 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146 Writing Definitions in Isabelle/HOL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 5 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 5.1 Recursive Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 5.2 Primitive Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156 5.3 Least and Greatest Fixed Points . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 5.4 Defining Continuous Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 5.5 Inductive and Coinductive Relation Definitions . . . . . . . . . . . . . . . . . . 172 5.6 Rule-Oriented Inductive and Coinductive Relation Definitions . . . . . 175 5.7 Inductive and Coinductive Function Definitions . . . . . . . . . . . . . . . . . 180 5.8 Inductive and Coinductive Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 Recursive Definitions in Isabelle/HOL . . . . . . . . . . . . . . . . . . . . . . . . . . . . 197 Part II The Higher Planes 6 Abstract Data Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206 6.2 Declarations, Signatures, and Presentations . . . . . . . . . . . . . . . . . . . . . 210 6.3 Algebras, Homomorphisms, and Abstract Data Types . . . . . . . . . . . . 216 6.4 Loose Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224 6.5 Generated and Free Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 230 6.6 Cogenerated and Cofree Specifications . . . . . . . . . . . . . . . . . . . . . . . . . 241 6.7 Specifying in the Large . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257

Contents xix 6.8 Reasoning about Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 278 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 304 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 304 Abstract Data Types in CafeOBJ and CASL . . . . . . . . . . . . . . . . . . . . . . . 307 7 Programming Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 319 7.1 Programs and Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 320 7.2 A Denotational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 323 7.3 An Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 342 7.4 The Correctness of Translations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 361 7.5 Procedures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 384 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 405 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 405 Language Semantics in OCaml, the K Framework, and SLANG . . . . . 407 8 Computer Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 423 8.1 Specifying Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 424 8.2 Verifying Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 430 8.3 Predicate Transformers and Commands as Relations . . . . . . . . . . . . . 445 8.4 Non-Abortion and Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 463 8.5 Loop Invariants and Termination Measures . . . . . . . . . . . . . . . . . . . . . 471 8.6 The Refinement of Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 491 8.7 Reasoning about Procedures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 498 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 507 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 507 Program Reasoning in RISCAL and the RISC ProgramExplorer . . . . 509 9 Concurrent Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 523 9.1 Labeled Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 524 9.2 Modeling Shared Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 539 9.3 Modeling Distributed Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 547 9.4 Specifying System Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 559 9.5 Verifying Invariance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 576 9.6 Verifying Response . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 588 9.7 The Refinement of Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 599 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 606 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 606 System Analysis in TLA+ and RISCAL . . . . . . . . . . . . . . . . . . . . . . . . . . . 609 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 625 Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 637

Logic for Programming: A Perspective Wer nicht von dreitausend Jahren sich weiß Rechenschaft zu geben, bleib im Dunkeln unerfahren, mag von Tag zu Tage leben. (Who cannot draw on three thousand years may stay in the dark, inexperienced, living from day to day.) — Johann Wolfgang von Goethe (West-östlicher Divan) Reading this book may be conceived as traveling through a landscape of unfamiliar domains. Even if the relevance of these domains to computer programming will be continuously emphasized and also demonstrated by various software presentations, the reader may be more motivated to undertake this voyage, if she has some perspective on “where the journey is heading”. Therefore this section will demonstrate some “real-life” applications of logic to modeling and reasoning about computer programs, in particular also examples of industrial relevance. However, of equal importance is the dual understanding of “where the journey has started”; we will therefore begin with a short historical account on the creation of logic and its evolution to a tool of computer science. While this presentation is certainly incomplete and also influenced by the goals of this book and the personal preferences of its author, it may convey to the reader a first “big picture” of the landscape through which we are walking. Logic and Language Logic (from the Greek word “logos” which may be translated as “reason”) emerged in antiquity from the human desire to distinguish a valid “argument” from an invalid one. Initially such arguments were expressed in natural language and were intended for everyday discourse, but also for discussing philosophical and scientific questions (“philosophical logic”); the development of formal (“symbolic” or “mathematical”) logic occurred at much later times. The roots of logic in the “Western” world (there have been alternative “Eastern” traditions in India and China) go back to the ancient Greece of the 4th century BCE. At that time, the Greek philosopher Aristotle developed in his writings later called “Organon” a theory of “syllogisms”; a syllogism is a particular form of logical argument that derives from two sentences, the “premises”, a third sentence, the “conclusion”. These sentences have the form of particular subject-predicate statements, namely “every 𝐴 is 𝐵” or “some 𝐴 is 𝐵”, respectively their negations; here 𝐴 and 𝐵 are “terms” that represent some basic concept like “human” or “mortal”, thus “every human is mortal” would be such a sentence. Although the expressiveness 1