The Denotational Description of Programming Languages: An Introduction

1. Introduction.- 1.1. Syntax, semantics and pragmatics.- 1.2. The purposes of formal semantics.- 1.2.1. Providing precise and machine-independent concepts.- 1.2.2. Providing unambiguous specification techniques.- 1.2.3. Providing a rigorous theory to support reliable reasoning.- 1.3. Denotational semantics.- 1.4. Abstract entities and their description.- 2. A first example: the language TINY.- 2.1. Informal syntax of TINY.- 2.2. Informal semantics of TINY.- 2.2.1. Informal semantics of expressions.- 2.2.2. Informal semantics of commands.- 2.3. An example.- 2.4. Formal semantics of TINY.- 2.4.1. Syntax.- 2.4.2. States, memories, inputs, outputs and values.- 2.4.3. Semantic functions.- 2.4.3.1. Denotations of expressions.- 2.4.3.2. Denotations of commands.- 2.4.4. Semantic clauses.- 2.4.4.1. Clauses for expressions.- 2.4.4.2. Clauses for commands.- 2.4.5. Summary of the formal semantics of TINY.- 3. General concepts and notation.- 3.1. Abstract syntax.- 3.2. Sets and domains.- 3.2.1. The problem of recursively defined functions.- 3.2.2. The problem of recursively defined sets.- 3.2.3. The role of Dana Scott's theory.- 3.2.4. The role of mathematics in this book.- 3.3. Defining domains.- 3.3.1. Standard domains.- 3.3.2. Finite domains.- 3.3.3. Domain constructors.- 3.3.3.1. Function space [D1?D2].- 3.3.3.2. Product [D1× D2×... × Dn].- 3.3.3.3. Sequences D*.- 3.3.4. Sum [D1+ D2+... + Dn].- 3.3.4. Domain equations.- 3.4. Functions.- 3.4.1. ?-notation.- 3.4.1.1. Basic idea.- 3.4.1.2. Elaborations.- 3.4.1.2.1. Explicitly indicating source and/or target.- 3.4.1.2.2. More than one argument.- 3.4.1.3. Applying ?-expressions to arguments.- 3.4.1.4. Changing bound variables.- 3.4.2. Higher order functions.- 3.4.3. Important notational conventions on precedence and association.- 3.4.4. Currying.- 3.4.5. Conditionals.- 3.4.6. Cases notation.- 3.4.7. Updating functions.- 3.4.8. Generic functions.- 3.4.9. Ways of defining functions (including recursion).- 3.4.10. Cancelling out variables.- 3.4.11. where notation.- 3.4.12. Composition and sequencing.- 3.4.12.1. Composition.- 3.4.12.2. Sequencing.- 4. Denotational description of TINY.- 4.1. Abstract syntax.- 4.1.1. Syntactic domains.- 4.1.2. Syntactic clauses.- 4.2. Semantics.- 4.2.1. Semantic domains.- 4.2.2. Auxiliary functions.- 4.2.2.1. result.- 4.2.2.2. donothing.- 4.2.2.3. checkNum.- 4.2.2.4. checkBool.- 4.2.3. Semantic functions.- 4.2.4. Semantic clauses.- 4.2.4.1. Clauses for expressions.- 4.2.4.2. Clauses for commands.- 5. Standard semantics.- 5.1. Continuations.- 5.1.1. Modelling the 'rest of the program'.- 5.1.2. Direct and continuation semantics.- 5.1.3. Continuation semantics of TINY.- 5.1.3.1. Semantic domains and functions.- 5.1.3.2. Semantic clauses.- 5.1.4. Final answers and output.- 5.1.4.1. Final answers are not states.- 5.1.4.2. Output is not part of the state.- 5.1.4.3. Output can be infinite.- 5.2. Locations, stores and environments.- 5.2.1. Sharing.- 5.2.2. Variables and locations.- 5.2.3. Stores.- 5.2.4. Environments.- 5.3. Standard domains of values.- 5.4. Blocks, declarations and scope.- 5.5. Standard domains of continuations.- 5.5.1. Command continuations.- 5.5.2. Expression continuations.- 5.5.3. Declaration continuations.- 5.6. Standard semantic functions.- 5.7. Continuation transforming functions.- 5.7.1. cont.- 5.7.2. update.- 5.7.3. ref.- 5.7.4. deref.- 5.7.5. err.- 5.7.6. Domain checks: D?.- 5.8. Assignments and L and R values.- 5.8.1. L and R values.- 5.9. Procedures and functions.- 5.9.1. Procedures.- 5.9.2. Functions.- 5.9.3. Summary.- 5.10 Non standard semantics and concurrency.- 6. A second example: the language SMALL.- 6.1. Syntax of SMALL.- 6.1.1. Syntactic domains.- 6.1.2. Syntactic clauses.- 6.2. Semantics of SMALL.- 6.2.1. Semantic domains.- 6.2.2. Semantic functions.- 6.2.3. Semantic clauses.- 6.2.3.1. Programs.- 6.2.3.2. Expressions.- 6.2.3.3. Commands.- 6.2.3.4. Declarations.- 6.3. A worked example.- 7. Escapes and jumps.- 7.1. Escapes.- 7.1.1. Escapes from commands.- 7.1.2. Escapes from expressions.- 7.1.3. valof and resultis.- 7.2. Jumps.- 7.2.1 The semantics of jumps.- 7.2.2. Assigning label values to variables.- 8. Various kinds of procedures and functions.- 8.1. Procedures (or functions) with zero or more parameters.- 8.1.1. Zero parameters.- 8.1.2. More than one parameter.- 8.2. Recursive procedures and functions.- 8.2.1. Recursive functions in ALGOL 60 and PASCAL.- 8.3. Static and dynamic binding.- 8.3.1. Semantics of binding.- 8.3.2. Advantages and disadvantages of dynamic binding.- 8.4. Parameter passing mechanisms.- 8.4.1. Call by value.- 8.4.2. Call by reference.- 8.4.2.1. Simple call by reference.- 8.4.2.2. PASCAL call by reference.- 8.4.2.3. FORTRAN call by reference.- 8.4.3. Call by value and result.- 8.5. Procedure calling mechanisms.- 8.5.1. Call by closure (ALGOL 60 call by name).- 8.5.2. Call by text (LISP FEXPRs).- 8.5.3. Call by denotation.- 8.5.4. Quotation constructs.- 8.6. Summary of calling and passing mechanisms.- 8.7. Procedure and function denoting expressions (abstractions).- 8.8. Declaration binding mechanisms.- 9. Data structures.- 9.1. References.- 9.2. Arrays.- 9.2.1. news.- 9.2.2. newarray.- 9.2.3. subscript.- 9.3. Records.- 9.4. Data structure valued expressions.- 9.5. Files.- 10. Iteration constructs.- 10.1. repeat C until E.- 10.2. Event loops.- 10.3. For-statements.- 11. Own-variables.- 11.1. The within construct.- 11.2. Different interpretations of ALGOL 60 own-variables.- 11.3. Semantics of own-variables.- 11.3.1. Static interpretation.- 11.3.2. Intermediate interpretation.- 11.3.3. Dynamic interpretation.- 12. Types.- 12.1. Various kinds of types.- 12.2. Well-typed programs and type-checking.- 12.2.1. The denotational description of type-checking.- 12.3. The semantics of types.- Appendix: Remarks for instructors and sample exercises.- Sample exercises.- References.- Subject and Author Index.- Symbols.