Cliff B. Jones: Understanding Programming Languages
Springer, November 2020, 229 pp, ISBN: 978-3-030-59256-1. https://doi.org/10.1007/978-3-030-59257-8
Summary
The book Understanding Programming Languages by Cliff B. Jones is about the formal specification of the semantics of programming languages. It focuses on the structural operational semantics of imperative and sequential languages, including features such as blocks and procedures, with an extension to concurrent objects at the end of the book. The material is presented with great clarity and requires almost no background knowledge, making the book perfectly suitable for any person curious about programming languages and seeking a deeper understanding of how they work. This book is also for language designers, as being formally precise is an invaluable tool to help catch design issues early in the design phase.
This review is written by Alan Schmitt for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community.
Understanding Programming Languages
by
Cliff B. Jones.
Review
The book Understanding Programming Languages by Cliff B. Jones is about the formal specification of the semantics of programming languages. Many formal frameworks exist to describe semantics. This book focuses on structural operational semantics: a description of the computation steps taken by programming constructs which is derived from the structure of the program. Other semantic approaches are touched upon, such as denotational semantics and axiomatic semantics, but they are not studied in detail. The book also mostly tackles imperative and sequential languages, including features such as blocks and procedures, with an extension to concurrent objects at the end of the book.
To go into more detail, the book is composed of 11 chapters and 6 appendices. The first chapter introduces the metalanguage used in the rest of the book. This language is based on the Vienna Development Method. The formalization of program text, i.e., syntax, is then described using Backus-Naur Form rules in the second chapter. This is where the first “Challenge” and “Language Issue” boxes are encountered: these short paragraphs highlight crucial points and potential pitfalls when designing a language. The book includes 8 challenges and 46 language issues, helpfully typeset in different colors. The next two chapters finish setting up the formal foundations. Chapter 3 introduces a way to give meaning to programs, in the form of an operational semantics. The particular flavor of semantics chosen is structural operational semantics in a big-step style, where a relation between program text and final results is defined (denotational and axiomatic semantics are described in Chapter 7). Chapter 4 talks about static semantics, or typing, to rule out meaningless programs without having to run them. The approach is shown to adapt to additional features such as input/output, arrays, and records. Chapters 5 and 6 introduce features of programming languages that present additional challenges to model, including blocks (with local variables and thus a notion of scope), non-recursive procedures with multiple parameter passing styles, functions, and heap variables. Chapters 8 and 9 turn to concurrency. To this end, the operational semantics is now in a small-step style. This style relates configurations, i.e., program text and state, to configurations after some computation. Small-step semantics are used to describe the partial execution of code in order to model interleaving. A concurrent semantics for an object-oriented language is proposed, where the granularity of the concurrency is at the object level (there is at most one method active per object) and the granularity of thread switching is at the statement level (no switching is allowed during the evaluation of expressions). Finally, Chapter 10 briefly mentions complex control-flow issues, such as exceptions or goto statements, before the concluding chapter. The appendices helpfully collect notations, formal semantics, and additional notes. In addition, each chapter proposes some projects to continue exploring the material presented.
Although many aspects of the semantics of programming languages are covered in depth and with a remarkable clarity, the book is not without shortcomings. In particular, keeping with its pedagogical and foundational point of view, the book could have continued building towards more advanced topics, providing non-technical overviews or including pointers to additional resources. These advanced topics may include the explicit handling of continuations, which is increasingly present in mainstream languages in the form of coroutines, generators, or algebraic effects. Similarly, the semantics of functional languages could have been mentioned or studied in more depth, especially considering that many elements, like the notion of environment, are already present to tackle this issue. This would have paved the way to formally addressing the question of recursion, which is mentioned only briefly. Since the book targets an audience without necessarily a background in formal semantics, these more advanced topics have unfortunately been left out, or only hinted at. They could be considered as additional material for a future, second edition of the book.
Last but not least, I really enjoyed the historical notes describing the early days of operational semantics. Putting the concepts developed in the book in historical context significantly enhances the narrative.
To sum up, this book is an introduction to the structural operational semantics of imperative languages. The material is presented with great clarity and requires almost no background knowledge, making the book perfectly suitable for any person curious about programming languages and seeking a deeper understanding of how they work. This book is also for language designers, as being formally precise is an invaluable tool to help catch design issues early in the design phase.