Preface | ix | |

1 | Predicate Logic | 1 |
---|---|---|

1.1 | Abstract Syntax | 1 |

1.2 | Denotational Semantics of Predicate Logic | 8 |

1.3 | Validity and Inference | 12 |

1.4 | Binding and Substitution | 15 |

2 | The Simple Imperative Language | 24 |

2.1 | Syntax | 24 |

2.2 | Denotational Semantics | 26 |

2.3 | Domains and Continuous Functions | 29 |

2.4 | The Least Fixed-Point Theorem | 35 |

2.5 | Variable Declarations and Substitution | 39 |

2.6 | Syntactic Sugar: The for Command | 45 |

2.7 | Arithmetic Errors | 47 |

2.8 | Soundness and Full Abstraction | 48 |

3 | Program Specifications and Their Proofs | 54 |

3.1 | Syntax and Semantics of Specifications | 55 |

3.2 | Inference Rules | 57 |

3.3 | Rules for Assignment and Sequential Composition | 57 |

3.4 | Rules for while Commands | 63 |

3.5 | Further Rules | 66 |

3.6 | Computing Fibonacci Numbers | 69 |

3.7 | Fast Exponentiation | 71 |

3.8 | Complications and Limitations | 74 |

4 | Arrays | 81 |

4.1 | Abstract Syntax | 81 |

4.2 | Denotational Semantics | 83 |

4.3 | Binary Search | 85 |

4.4 | Inference Rules for Arrays | 90 |

4.5 | Higher-Order Assertions About Arrays | 93 |

5 | Failure, Input-Output, and Continuations | 97 |

5.1 | The fail Command | 97 |

5.2 | Intermediate Output and a Domain of Sequences | 101 |

5.3 | The Physical Argument for Continuity | 107 |

5.4 | Products and Disjoint Unions of Predomains | 109 |

5.5 | Recursive Domain Isomorphisms | 111 |

5.6 | Intermediate Input and a Domain of Resumptions | 113 |

5.7 | Continuation Semantics | 115 |

5.8 | Continuation Semantics of Extensions | 118 |

6 | Transition Semantics | 126 |

6.1 | Configurations and the Transition Relation | 126 |

6.2 | Inference Rules for the Simple Language | 127 |

6.3 | Transition Semantics of fail | 131 |

6.4 | Input and Output | 132 |

7 | Nondeterminism and Guarded Commands | 136 |

7.1 | Syntax and Transition Semantics | 137 |

7.2 | Bounded Nondeterminism and Powerdomains | 139 |

7.3 | Semantic Equations | 144 |

7.4 | Program Specification and Proof | 147 |

7.5 | Weakest Preconditions | 149 |

8 | Shared-Variable Concurrency | 155 |

8.1 | Concurrent Composition | 155 |

8.2 | Critical Regions | 157 |

8.3 | Mutual Exclusion and Conditional Critical Regions | 159 |

8.4 | Deadlock | 161 |

8.5 | Fairness | 162 |

8.6 | Resumption Semantics | 164 |

8.7 | Transition Traces | 165 |

8.8 | Stuttering and Mumbling | 171 |

9 | Communicating Sequential Processes | 181 |

9.1 | Syntax | 181 |

9.2 | Transition Semantics | 183 |

9.3 | Possible Restrictions | 187 |

9.4 | Examples | 188 |

9.5 | Deadlock | 189 |

9.6 | Fairness | 189 |

10 | The Lambda Calculus | 194 |

10.1 | Syntax | 196 |

10.2 | Reduction | 197 |

10.3 | Normal-Order Evaluation | 201 |

10.4 | Eager Evaluation | 206 |

10.5 | Denotational Semantics | 208 |

10.6 | Programming in the Lambda Calculus | 216 |

11 | An Eager Functional Language | 222 |

11.1 | Concrete Syntax | 222 |

11.2 | Evaluation Semantics | 223 |

11.3 | Definitions, Patterns, and Recursion | 228 |

11.4 | Lists | 231 |

11.5 | Examples | 232 |

11.6 | Direct Denotational Semantics | 235 |

11.7 | Dynamic Binding | 242 |

12 | Continuations in a Functional Language | 251 |

12.1 | Continuation Semantics | 251 |

12.2 | Continuations as Values | 255 |

12.3 | Continuations as a Programming Technique | 257 |

12.4 | Deriving a First-Order Semantics | 258 |

12.5 | First-Order Semantics Summarized | 264 |

12.6 | Relating First-Order and Continuation Semantics | 269 |

13 | Iswim-like Languages | 273 |

13.1 | Aliasing, References, and States | 273 |

13.2 | Evaluation Semantics | 276 |

13.3 | Continuation Semantics | 278 |

13.4 | Some Syntactic Sugar | 282 |

13.5 | First-Order Semantics | 282 |

13.6 | Examples | 284 |

13.7 | Exceptions | 287 |

13.8 | Backtracking | 289 |

13.9 | Input and Output | 291 |

13.10 | Some Complications | 293 |

14 | A Normal-Order Language | 298 |

14.1 | Evaluation Semantics | 298 |

14.2 | Syntactic Sugar | 301 |

14.3 | Examples | 302 |

14.4 | Direct Denotational Semantics | 304 |

14.5 | Reduction Revisited | 306 |

14.6 | Lazy Evaluation | 307 |

15 | The Simple Type System | 315 |

15.1 | Types, Contexts, and Judgements | 316 |

15.2 | Inference Rules | 318 |

15.3 | Explicit Typing | 324 |

15.4 | The Extrinsic Meaning of Types | 327 |

15.5 | The Intrinsic View | 334 |

15.6 | Set-Theoretic Semantics | 339 |

15.7 | Recursive Types | 341 |

16 | Subtypes and Intersection Types | 349 |

16.1 | Inference Rules for Subtyping | 349 |

16.2 | Named Products and Sums | 352 |

16.3 | Intersection Types | 354 |

16.4 | Extrinsic Semantics | 358 |

16.5 | Generic Operators | 362 |

16.6 | Intrinsic Semantics | 365 |

17 | Polymorphism | 379 |

17.1 | Syntax and Inference Rules | 380 |

17.2 | Polymorphic Programming | 383 |

17.3 | Extrinsic Semantics | 390 |

18 | Module Specification | 398 |

18.1 | Type Definitions | 398 |

18.2 | Existential Quantification and Modules | 401 |

18.3 | Implementing One Abstraction in Terms of Another | 406 |

19 | Algol-like Languages | 415 |

19.1 | Data Types and Phrase Types | 416 |

19.2 | Phrases and Type Inference Rules | 419 |

19.3 | Examples | 423 |

19.4 | Arrays and Declarators | 426 |

19.5 | A Semantics Embodying the Stack Discipline | 428 |

19.6 | The Semantics of Variables | 434 |

19.7 | The Semantics of Procedures | 436 |

19.8 | Some Extensions and Simplifications | 439 |

Appendix: Mathematical Background | 447 | |

A.1 | Sets | 448 |

A.2 | Relations | 450 |

A.3 | Functions | 452 |

A.4 | Relations and Functions Between Sets | 456 |

A.5 | More About Products and Disjoint Unions | 459 |

A.6 | More About Relations | 462 |

Bibliography | 467 | |

Index | 483 |

last updated February 7, 1999