This book is about describing the meaning of programming languages. The author teaches the skill of writing semantic descriptions as an efficient way to understand the features of a language. While a compiler or an interpreter offers a form of formal description of a language, it is not something that can be used as a basis for reasoning about that language nor can it serve as a definition of a programming language itself since this must allow a range of implementations. By writing a formal semantics of a language a designer can yield a far shorter description and tease out, analyse and record design choices.
Early in the book the author introduces a simple notation, a meta-language, used to record descriptions of the semantics of languages. In a practical approach, he considers dozens of issues that arise in current programming languages and the key techniques that must be mastered in order to write the required formal semantic descriptions. The book concludes with a discussion of the eight key challenges: delimiting a language (concrete representation), delimiting the abstract content of a language, recording semantics (deterministic languages), operational semantics (non-determinism), context dependency, modelling sharing, modelling concurrency, and modelling exits.
The content is class-tested and suitable for final-year undergraduate and postgraduate courses. It is also suitable for any designer who wants to understand languages at a deep level. Most chapters offer projects, some of these quite advanced exercises that ask for complete descriptions of languages, and the book is supported throughout with pointers to further reading and resources. As a prerequisite the reader should know at least one imperative high-level language and have some knowledge of discrete mathematics notation for logic and set theory.
Author(s): Cliff B. Jones
Publisher: Springer
Year: 2020
Language: English
Pages: 229
City: Cham
Preface
Using this book
Writing style
Acknowledgements
Contents
Chapter 1 Programming languages and their description
1.1 Digital computers and programming languages
1.2 The importance of HLLs
1.3 Translators, etc.
1.4 Insights from natural languages
1.5 Approaches to describing semantics
1.6 A meta-language
1.7 Further material
1.7.1 Further reading
1.7.2 Classes of languages
1.7.3 Logic of Partial Functions
Chapter 2 Delimiting a language
2.1 Concrete syntax
2.2 Abstract syntax
2.3 Further material
Projects
Further reading
Historical notes
Chapter 3 Operational semantics
3.1 Operational semantics
3.2 Structural Operational Semantics
3.2.1 Relations
3.2.2 Inference rules
3.2.3 Non-deterministic iteration
3.3 Further material
Projects
Alternatives
Further reading
Historical notes
Chapter 4 Constraining types
4.1 Static vs. dynamic error detection
4.2 Context conditions
4.3 Semantic objects
4.3.1 Input/output
4.3.2 Arrays
4.3.3 Records
4.4 Further material
Projects
Further reading
Chapter 5 Block structure
5.1 Blocks
5.2 Abstract locations
5.3 Procedures
5.4 Parameter passing
5.4.1 Passing “by reference”
5.4.2 Passing “by value”
5.5 Further material
Projects
Further reading
Chapter 6 Further issues in sequential languages
6.1 Own variables
6.2 Objects and methods
6.3 Pascal variant records
6.4 Heap variables
6.5 Functions
6.5.1 Marking the return value
6.5.2 Side effects
6.5.3 Recursion
6.5.4 Passing functions as parameters [*]
Procedure variables/results
6.6 Further material
Projects
Chapter 7 Other semantic approaches
7.1 Denotational semantics
7.2 Further material
7.3 The axiomatic approach
7.3.1 Assertions on states
7.3.2 Hoare’s axioms
7.3.3 Specification as statements
7.3.4 Formal development
7.3.5 Data abstraction and reification
7.4 Further material
7.5 Roles for semantic approaches
Chapter 8 Shared-variable concurrency
8.1 Interference
8.2 Small-step semantics
8.3 Granularity
8.4 Rely/Guarantee reasoning [*]
8.5 Concurrent Separation Logic [*]
8.6 Further material
Projects
Further reading
Chapter 9 Concurrent OOLs
9.1 Objects for concurrency
9.1.1 An example program
9.1.2 Semantic objects
9.2 Expressions
9.3 Simple statements
9.4 Creating objects
9.5 Method activation and synchronisation
9.5.1 Method activation
9.5.2 Method synchronisation
9.5.3 Delegation
9.6 Reviewing COOL
The example class
COOL summary
9.7 Further material
Chapter 10 Exceptional ordering [*]
10.1 Abnormal exit model
10.2 Continuations
10.3 Relating the approaches
10.4 Further material
Projects
Historical notes
Chapter 11 Conclusions
11.1 Review of challenges
11.2 Capabilities of formal description methods
11.3 Envoi
Appendix A Simple language
A.1 Concrete syntax
A.1.1 Dijkstra style
A.1.2 Java-style statement syntax
A.2 Abstract syntax
A.3 Semantics
Statements
Expressions
Appendix B Typed language
B.1 Abstract syntax
B.2 Context conditions
B.3 Semantics
Appendix C Blocks language
C.1 Auxiliary objects
Objects needed for context conditions
Semantic objects
C.2 Programs
C.3 Statements
C.4 Simple statements Assignment
C.5 Compound statements
C.6 Blocks
C.7 Call statements
C.8 Expressions
Appendix D COOL
Abbreviations
D.1 Auxiliary objects
Types for context conditions
Types for semantics
D.2 Expressions
D.3 Statements
D.3.1 Assignments
D.3.2 If statements
D.4 Methods
D.4.1 Activate method
D.4.2 Call method
D.4.3 Rendezvous
D.4.4 Method termination
D.4.5 Delegation
D.5 Classes
D.5.1 Creating objects
D.5.2 Discarding references
D.6 Programs
Appendix E VDM notation
E.1 Logical operators
E.2 Set notation
E.3 List (sequence) notation
E.4 Map notation
E.5 Record notation
E.6 Function notation
Appendix F Notes on influential people
References
Index
