| |
| |
| Series foreword | |
| |
| |
| Preface | |
| |
| |
| |
| Basic set theory | |
| |
| |
| |
| Logical notation | |
| |
| |
| |
| Sets | |
| |
| |
| |
| Relations and functions | |
| |
| |
| |
| Introduction to operational semantics | |
| |
| |
| |
| IMP - a simple imperative language | |
| |
| |
| |
| The evaluation of arithmetic expressions | |
| |
| |
| |
| The evaluation of boolean expressions | |
| |
| |
| |
| The execution of commands | |
| |
| |
| |
| A simple proof | |
| |
| |
| |
| Alternative semantics | |
| |
| |
| |
| Some principles of induction | |
| |
| |
| |
| Mathematical induction | |
| |
| |
| |
| Structural induction | |
| |
| |
| |
| Well-founded induction | |
| |
| |
| |
| Induction on derivations | |
| |
| |
| |
| Definitions by induction | |
| |
| |
| |
| Inductive definitions | |
| |
| |
| |
| Rule induction | |
| |
| |
| |
| Special rule induction | |
| |
| |
| |
| Proof rules for operational semantics | |
| |
| |
| |
| Operators and their least fixed points | |
| |
| |
| |
| The denotational semantics of IMP | |
| |
| |
| |
| Motivation | |
| |
| |
| |
| Denotational semantics | |
| |
| |
| |
| Equivalence of the semantics | |
| |
| |
| |
| Complete partial orders and continuous functions | |
| |
| |
| |
| The Knaster-Tarski Theorem | |
| |
| |
| |
| The axiomatic semantics of IMP | |
| |
| |
| |
| The idea | |
| |
| |
| |
| The assertion language Assn | |
| |
| |
| |
| Semantics of assertions | |
| |
| |
| |
| Proof rules for partial correctness | |
| |
| |
| |
| Soundness | |
| |
| |
| |
| Using the Hoare rules - an example | |
| |
| |
| |
| Completeness of the Hoare rules | |
| |
| |
| |
| Godel's Incompleteness Theorem | |
| |
| |
| |
| Weakest preconditions and expressiveness | |
| |
| |
| |
| Proof of Godel's Theorem | |
| |
| |
| |
| Verification conditions | |
| |
| |
| |
| Predicate transformers | |
| |
| |
| |
| Introduction to domain theory | |
| |
| |
| |
| Basic definitions | |
| |
| |
| |
| Streams - an example | |
| |
| |
| |
| Constructions on cpo's | |
| |
| |
| |
| A metalanguage | |
| |
| |
| |
| Recursion equations | |
| |
| |
| |
| The language REC | |
| |
| |
| |
| Operational semantics of call-by-value | |
| |
| |
| |
| Denotational semantics of call-by-value | |
| |
| |
| |
| Equivalence of semantics for call-by-value | |
| |
| |
| |
| Operational semantics of call-by-name | |
| |
| |
| |
| Denotational semantics of call-by-name | |
| |
| |
| |
| Equivalence of semantics for call-by-name | |
| |
| |
| |
| Local declarations | |
| |
| |
| |
| Techniques for recursion | |
| |
| |
| |
| Bekie's Theorem | |
| |
| |
| |
| Fixed-point induction | |
| |
| |
| |
| Well-founded induction | |
| |
| |
| |
| Well-founded recursion | |
| |
| |
| |
| Languages with higher types | |
| |
| |
| |
| An eager language | |
| |
| |
| |
| Eager operational semantics | |
| |
| |
| |
| Eager denotational semantics | |
| |
| |
| |
| Agreement of eager semantics | |
| |
| |
| |
| A lazy language | |
| |
| |
| |
| Lazy operational semantics | |
| |
| |
| |
| Lazy denotational semantics | |
| |
| |
| |
| Agreement of lazy semantics | |
| |
| |
| |
| Fixed-point operators | |
| |
| |
| |
| Observations and full abstraction | |
| |
| |
| |
| Sums | |
| |
| |
| |
| Information systems | |
| |
| |
| |
| Recursive types | |
| |
| |
| |
| Information systems | |
| |
| |
| |
| Closed families and Scott predomains | |
| |
| |
| |
| A cpo of information systems | |
| |
| |
| |
| Constructions | |
| |
| |
| |
| Recursive types | |
| |
| |
| |
| An eager language | |
| |
| |
| |
| Eager operational semantics | |
| |
| |
| |
| Eager denotational semantics | |
| |
| |
| |
| Adequacy of eager semantics | |
| |
| |
| |
| The eager [lambda]-calculus | |
| |
| |
| |
| A lazy language | |
| |
| |
| |
| Lazy operational semantics | |
| |
| |
| |
| Lazy denotational semantics | |
| |
| |
| |
| Adequacy of lazy semantics | |
| |
| |
| |
| The lazy [lambda]-calculus | |
| |
| |
| |
| Nondeterminism and parallelism | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| Guarded commands | |
| |
| |
| |
| Communicating processes | |
| |
| |
| |
| Milner's CCS | |
| |
| |
| |
| Pure CCS | |
| |
| |
| |
| A specification language | |
| |
| |
| |
| The modal [nu]-calculus | |
| |
| |
| |
| Local model checking | |
| |
| |
| A: Incompleteness and undecidability | |
| |
| |
| Bibliography | |
| |
| |
| Index | |