Preface
Chapter 0 INTRODUCTION
Methods for Semantics Specification
Suggested Readings
Chapter 1 SYNTAX
1.1 Abstract Syntax Definitions
1.2 Mathematical and Structural Induction
Suggested Readings
Exercises
Chapter 2 SETS, FUNCTIONS, AND DOMAINS
2.1 Sets
2.1.1 Constructions on Sets
2.2 Functions
2.2.1 Representing Functions as Sets
2.2.2 Representing Functions as Equations
2.3 Semantic Domains
2.3.1 Semantic Algebras
Suggested Readings
Exercises
Chapter 3 DOMAIN THEORY I: SEMANTIC ALGEBRAS
3.1 Primitive Domains
3.2 Compound Domains
3.2.1 Product
3.2.2 Disjoint Union
3.2.3 Function Space
3.2.4 Lifted Domains and Strictness
3.3 Recursive Function Definitions
3.4 Recursive Domain Definitions
3.5 Summary
Suggested Readings
Exercises
Chapter 4 BASIC STRUCTURE OF DENOTATIONAL DEFINITIONS
4.1 The Valuation Function
4.2 Format of a Denotational Definition
4.3 A Calculator Language
Suggested Readings
Exercises
Chapter 5 IMPERATIVE LANGUAGES
5.1 A Language with Assignment
5.1.1 Programs are Functions
5.2 An Interactive File Editor
5.2.1 Interactive Input and Partial Syntax
5.3 A Dynamically Typed Language with Input and Output
5.4 Altering the Properties of Stores
5.4.1 Delayed Evaluation
5.4.2 Retaining Multiple Stores
5.4.3 Noncommunicating Commands
Suggested Readings
Exercises
Chapter 6 DOMAIN THEORY II: RECURSIVELY DEFINED FUNCTIONS
6.1 Some Recursively Defined Functions
6.2 Partial Orderings
6.3 Continuous Functions
6.4 Least Fixed Points
6.5 Domains are Cpos
6.6 Examples
6.6.1 Factorial Function
6.6.2 Copyout Function
6.6.3 Double Recursion
6.6.4 Simultaneous Definitions
6.6.5 The While-Loop
6.6.6 Soundness of Hoare’s Logic
6.7 Reasoning about Least Fixed Points
Suggested Readings
Exercises
Chapter 7 LANGUAGES WITH CONTEXTS
7.1 A Block-Structured Language
7.1.1 Stack-Managed Storage
7.1.2 The Meanings of Identifiers
7.2 An Applicative Language
7.2.1 Scoping Rules
7.2.2 Self-Application
7.2.3 Recursive Declarations
7.3 Compound Data Structures
Suggested Readings
Exercises
Chapter 8 ABSTRACTION, CORRESPONDENCE, AND QUALIFICATION
8.1 Abstraction
8.1.1 Recursive Bindings
8.2 Parameterization
8.2.1 Polymorphism and Typing
8.3 Correspondence
8.4 Qualification
8.5 Orthogonality
Suggested Readings
Exercises
Chapter 9 CONTROL AS A SEMANTIC DOMAIN
9.1 Continuations
9.1.1 Other Levels of Continuations
9.2 Exception Mechanisms
9.3 Backtracking Mechanisms
9.4 Coroutine Mechanisms
9.5 Unrestricted Branching Mechanisms
9.6 The Relationship between Direct and Continuation Semantics
Suggested Readings
Exercises
Chapter 10 IMPLEMENTATION OF DENOTATIONAL DEFINITIONS
10.1 A General Method of Implementation
10.1.1 The SIS and SPS Systems
10.2 Static Semantics Processing
10.3 The Structure of the Evaluator
10.3.1 A Stack-Based Evaluator
10.3.2 PSP and Appel’s System
10.4 Combinator-Based Semantic Notations
10.4.1 The Plumb and CERES Systems
10.5 Transformations on the Semantic Definition
10.5.1 First-Order Data Objects
10.5.2 Global Variables
10.5.3 Control Structures
10.6 Implementation of Continuation-Based Definitions
10.6.1 The CGP and VDM Methods
10.7 Correctness of Implementation and Full Abstraction
Suggested Readings
Exercises
Chapter 11 DOMAIN THEORY III: RECURSIVE DOMAIN SPECIFICATIONS
11.1 Reflexive Domains Have Infinite Elements
11.2 The Inverse Limit Construction
11.3 Applications
11.3.1 Linear Lists
11.3.2 Self-Applicative Procedures
11.3.3 Recursive Record Structures
Suggested Readings
Exercises
Chapter 12 NONDETERMINISM AND CONCURRENCY
12.1 Powerdomains
12.2 The Guarded Command Language
12.3 Concurrency and Resumption Semantics
12.4 An Alternative Semantics for Concurrency
12.5 The Powerdomain Structure
12.5.1 Discrete Powerdomains
12.5.2 General Powerdomains
Suggested Readings
Exercises
Bibliography
· · · · · · (收起)