| Series foreword | |
| Preface | |
| Basic set theory | p. 1 |
| Logical notation | p. 1 |
| Sets | p. 2 |
| Relations and functions | p. 6 |
| Introduction to operational semantics | p. 11 |
| IMP - a simple imperative language | p. 11 |
| The evaluation of arithmetic expressions | p. 13 |
| The evaluation of boolean expressions | p. 17 |
| The execution of commands | p. 19 |
| A simple proof | p. 20 |
| Alternative semantics | p. 24 |
| Some principles of induction | p. 27 |
| Mathematical induction | p. 27 |
| Structural induction | p. 28 |
| Well-founded induction | p. 31 |
| Induction on derivations | p. 35 |
| Definitions by induction | p. 39 |
| Inductive definitions | p. 41 |
| Rule induction | p. 41 |
| Special rule induction | p. 44 |
| Proof rules for operational semantics | p. 45 |
| Operators and their least fixed points | p. 52 |
| The denotational semantics of IMP | p. 55 |
| Motivation | p. 55 |
| Denotational semantics | p. 56 |
| Equivalence of the semantics | p. 61 |
| Complete partial orders and continuous functions | p. 68 |
| The Knaster-Tarski Theorem | p. 74 |
| The axiomatic semantics of IMP | p. 77 |
| The idea | p. 77 |
| The assertion language Assn | p. 80 |
| Semantics of assertions | p. 84 |
| Proof rules for partial correctness | p. 89 |
| Soundness | p. 91 |
| Using the Hoare rules - an example | p. 93 |
| Completeness of the Hoare rules | p. 99 |
| Godel's Incompleteness Theorem | p. 99 |
| Weakest preconditions and expressiveness | p. 100 |
| Proof of Godel's Theorem | p. 110 |
| Verification conditions | p. 112 |
| Predicate transformers | p. 115 |
| Introduction to domain theory | p. 119 |
| Basic definitions | p. 119 |
| Streams - an example | p. 121 |
| Constructions on cpo's | p. 123 |
| A metalanguage | p. 135 |
| Recursion equations | p. 141 |
| The language REC | p. 141 |
| Operational semantics of call-by-value | p. 143 |
| Denotational semantics of call-by-value | p. 144 |
| Equivalence of semantics for call-by-value | p. 149 |
| Operational semantics of call-by-name | p. 153 |
| Denotational semantics of call-by-name | p. 154 |
| Equivalence of semantics for call-by-name | p. 157 |
| Local declarations | p. 161 |
| Techniques for recursion | p. 163 |
| Bekie's Theorem | p. 163 |
| Fixed-point induction | p. 166 |
| Well-founded induction | p. 174 |
| Well-founded recursion | p. 176 |
| Languages with higher types | p. 183 |
| An eager language | p. 183 |
| Eager operational semantics | p. 186 |
| Eager denotational semantics | p. 188 |
| Agreement of eager semantics | p. 190 |
| A lazy language | p. 200 |
| Lazy operational semantics | p. 201 |
| Lazy denotational semantics | p. 203 |
| Agreement of lazy semantics | p. 204 |
| Fixed-point operators | p. 209 |
| Observations and full abstraction | p. 215 |
| Sums | p. 219 |
| Information systems | p. 223 |
| Recursive types | p. 223 |
| Information systems | p. 225 |
| Closed families and Scott predomains | p. 228 |
| A cpo of information systems | p. 233 |
| Constructions | p. 236 |
| Recursive types | p. 251 |
| An eager language | p. 251 |
| Eager operational semantics | p. 255 |
| Eager denotational semantics | p. 257 |
| Adequacy of eager semantics | p. 262 |
| The eager [lambda]-calculus | p. 267 |
| A lazy language | p. 278 |
| Lazy operational semantics | p. 278 |
| Lazy denotational semantics | p. 281 |
| Adequacy of lazy semantics | p. 288 |
| The lazy [lambda]-calculus | p. 290 |
| Nondeterminism and parallelism | p. 297 |
| Introduction | p. 297 |
| Guarded commands | p. 298 |
| Communicating processes | p. 303 |
| Milner's CCS | p. 308 |
| Pure CCS | p. 311 |
| A specification language | p. 316 |
| The modal [nu]-calculus | p. 321 |
| Local model checking | p. 327 |
| A: Incompleteness and undecidability | p. 337 |
| Bibliography | p. 353 |
| Index | p. 357 |
| Table of Contents provided by Blackwell. All Rights Reserved. |