The Formal Semantics of Programming Languages provides the basic mathematical techniques necessary for those who are beginning a study of the semantics and logics of programming languages. These techniques will allow students to invent, formalize, and justify rules with which to reason about a variety of programming languages. Although the treatment is elementary, several of the topics covered are drawn from recent research, including the vital area of concurency. The book contains many exercises ranging from simple to miniprojects. Starting with basic set theory, structural operational semantics is introduced as a way to define the meaning of programming languages along with associated proof techniques. Denotational and axiomatic semantics are illustrated on a simple language of while-programs, and fall proofs are given of the equivalence of the operational and denotational semantics and soundness and relative completeness of the axiomatic semantics. A proof of Godel's incompleteness theorem, which emphasizes the impossibility of achieving a fully complete axiomatic semantics, is included. It is supported by an appendix providing an introduction to the theory of computability based on while-programs. Following a presentation of domain theory, the semantics and methods of proof for several functional languages are treated. The simplest language is that of recursion equations with both call-by-value and call-by-name evaluation. This work is extended to lan guages with higher and recursive types, including a treatment of the eager and lazy lambda-calculi. Throughout, the relationship between denotational and operational semantics is stressed, and the proofs of the correspondence between the operation and denotational semantics are provided. The treatment of recursive types - one of the more advanced parts of the book - relies on the use of information systems to represent domains. The book concludes with a chapter on parallel programming languages, accompanied by a discussion of methods for specifying and verifying nondeterministic and parallel programs.
Author(s): Glynn Winskel
Publisher: The MIT Press
Year: 1993
Language: English
Pages: 384
Cover......Page 1
Foundations of Computing......Page 3
The Formal Semantics of Programming Languages: An Introduction......Page 4
0262231697......Page 5
Contents......Page 8
Series foreword......Page 14
Preface......Page 16
1.1 Logical notation ......Page 22
1.2 Sets ......Page 23
1.2.2 Some important sets ......Page 24
1.2.3 Constructions on sets ......Page 25
1.3 Relations and functions ......Page 27
1.3.2 Composing relations and functions ......Page 28
1.3.4 Equivalence relations ......Page 30
1.4 FUrther reading ......Page 31
2.1 IMP-a simple imperative language ......Page 32
2.2 The evaluation of arithmetic expressions ......Page 34
2.3 The evaluation of boolean expressions ......Page 38
2.4 The execution of commands ......Page 40
2.5 A simple proof ......Page 41
2.6 Alternative semantics ......Page 45
2.7 Further reading......Page 47
3.1 Mathematical induction ......Page 48
3.2 Structural induction ......Page 49
3.3 Well-founded induction ......Page 52
3.4 Induction on derivations ......Page 56
3.5 Definitions by induction ......Page 60
3.6 Further reading ......Page 61
4.1 Rule induction ......Page 62
4.2 Special rule induction ......Page 65
4.3.1 Rule induction for arithmetic expressions ......Page 66
4.3.2 Rule induction for boolean expressions ......Page 67
4.3.3 Rule induction for commands ......Page 68
4.4 Operators and their least fixed points ......Page 73
4.5 Further reading ......Page 75
5.1 Motivation ......Page 76
5.2 Denotational semantics ......Page 77
5.3 Equivalence of the semantics ......Page 82
5.4 Complete partial orders and continuous functions ......Page 89
5.5 The Knaster-Tarski Theorem ......Page 95
5.6 Further reading ......Page 96
6.1 The idea ......Page 98
6.2 The assertion language Assn ......Page 101
6.2.1 Free and bound variables ......Page 102
6.2.2 Substitution ......Page 103
6.3 Semantics of assertions ......Page 105
6.4 Proof rules for partial correctness ......Page 110
6.5 Soundness ......Page 112
6.6 Using the Hoare rules-an example ......Page 114
6.7 Further reading ......Page 117
7.1 Codel's Incompleteness Theorem ......Page 120
7.2 Weakest preconditions and expressiveness ......Page 121
7.3 Proof of Codel's Theorem ......Page 131
7.4 Verification conditions ......Page 133
7.5 Predicate transformers ......Page 136
7.6 Further reading ......Page 138
8.1 Basic definitions ......Page 140
8.2 Streams-an example ......Page 142
8.3 Constructions on cpo's ......Page 144
8.3.1 Discrete cpo's ......Page 145
8.3.2 Finite products ......Page 146
8.3.3 Function space ......Page 149
8.3.4 Lifting ......Page 152
8.3.5 Sums ......Page 154
8.4 A metalanguage ......Page 156
8.5 Further reading ......Page 160
9.1 The language REC ......Page 162
9.2 Operational semantics of call-by-value ......Page 164
9.3 Denotational semantics of call-by-value ......Page 165
9.4 Equivalence of semantics for call-by-value ......Page 170
9.5 Operational semantics of call-by-name ......Page 174
9.6 Denotational semantics of call-by-name ......Page 175
9.7 Equivalence of semantics for call-by-name ......Page 178
9.8 Local declarations ......Page 182
9.9 Further reading ......Page 183
10.1 Bekic's Theorem......Page 184
10.2 Fixed-point induction ......Page 187
10.3 Well-founded induction ......Page 195
10.4 Well-founded recursion ......Page 197
10.5 An exercise ......Page 200
10.6 Further reading ......Page 202
11.1 An eager language ......Page 204
11.2 Eager operational semantics ......Page 207
11.3 Eager denotational semantics ......Page 209
11.4 Agreement of eager semantics ......Page 211
11.5 A lazy language ......Page 221
11.6 Lazy operational semantics ......Page 222
11.7 Lazy denotational semantics ......Page 224
11.8 Agreement of lazy semantics ......Page 225
11.9 Fixed-point operators ......Page 230
11.10 Observations and full abstraction ......Page 236
11.11 Sums ......Page 240
11.12 Further reading ......Page 242
12.1 Recursive types ......Page 244
12.2 Information systems ......Page 246
12.3 Closed families and Scott predomains ......Page 249
12.4 A cpo of information systems ......Page 254
12.5 Constructions ......Page 257
12.5.1 Lifting ......Page 258
12.5.2 Sums ......Page 260
12.5.3 Product ......Page 262
12.5.4 Lifted function space ......Page 264
12.6 Further reading ......Page 270
13.1 An eager language ......Page 272
13.2 Eager operational semantics ......Page 276
13.3 Eager denotational semantics ......Page 278
13.4 Adequacy of eager semantics ......Page 283
13.5 The eager A-calculus ......Page 288
13.5.1 Equational theory ......Page 290
13.5.2 A fixed-point operator ......Page 293
13.7 Lazy operational semantics ......Page 299
13.8 Lazy denotational semantics ......Page 302
13.9 Adequacy of lazy semantics ......Page 309
13.10 The lazy λ-calculus......Page 311
13.10.1 Equational theory ......Page 312
13.10.2 A fixed-point operator ......Page 313
13.11 Further reading ......Page 316
14.1 Introduction ......Page 318
14.2 Guarded commands ......Page 319
14.3 Communicating processes ......Page 324
14.4 Milner's CCS ......Page 329
14.5 Pure CCS ......Page 332
14.6 A specification language ......Page 337
14.7 The modal v-calculus ......Page 342
14.8 Local model checking ......Page 348
14.9 Further reading ......Page 356
A.1 Computability......Page 358
A.2 Undecidability......Page 360
A.3 Godel's incompleteness theorem......Page 364
A.4 A universal program......Page 366
A.5 Matijasevic's Theorem......Page 368
A.6 Further reading......Page 372
Bibliography ......Page 374
Index ......Page 378
