Название: Thinking Programs: Logical Modeling and Reasoning About Languages, Data, Computations, and Executions
Автор: Wolfgang Schreiner
Издательство: Springer
Год: 2021
Страниц: 660
Язык: английский
Формат: pdf (true)
Размер: 10.8 MB

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.

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.