상세정보

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.

정보제공 :

CONTENTS
Series foreword = xiii
Preface = xv
1 Basic set theory = 1
  1.1 Logical notation = 1
  1.2 Sets = 2
    1.2.1 Sets and properties = 3
    1.2.2 Some important sets = 3
    1.2.3 Constructions on sets = 4
    1.2.4 The axiom of foundation = 6
  1.3 Relations and functions = 6
    1.3.1 Lambda notation = 7
    1.3.2 Composing relations and functions = 7
    1.3.3 Direct and inverse image of a relation = 9
    1.3.4 Equivalence relations = 9
  1.4 Further reading = 10
2 Introduction to operational semantics = 11
  2.1 IMP ―a simple imperative language = 11
  2.2 The evaluation of arithmetic expressions = 13
  2.3 The evaluation of boolean expressions = 17
  2.4 The execution of commands = 19
  2.5 A simple proof = 20
  2.6 Alternative semantics = 24
  2.7 Further reading = 26
3 Some principles of induction = 27
  3.1 Mathematical induction = 27
  3.2 Structural induction = 28
  3.3 Well-founded induction = 31
  3.4 Induction on derivations = 35
  3.5 Definitions by induction = 39
  3.6 Further reading = 40
4 Inductive definitions = 41
  4.1 Rule induction = 41
  4.2 Special rule induction = 44
  4.3 Proof rules for operational semantics = 45
    4.3.1 Rule induction for arithmetic expressions = 45
    4.3.2 Rule induction for boolean expressions = 46
    4.3.3 Rule induction for commands = 47
  4.4 Operators and their least fixed points = 52
  4.5 Further reading = 54
5 The denotational semantics of IMP = 55
  5.1 Motivation = 55
  5.2 Denotational semantics = 56
  5.3 Equivalence of the semantic = 61
  5.4 Complete partial order and continuous functions = 68
  5.5 The Knaster-Theorem = 74
  5.6 Further reading = 75
6 The axiomatic semantics of IMP = 77
  6.1 The idea = 77
  6.2 The assertion language Assn = 80
    6.2.1 Free and bound variables = 81
    6.2.2 Substitution = 82
  6.3 Semantics of assertions = 84
  6.4 Proof rules for partial correctness = 89
  6.5 Soundness = 91
  6.6 Using the Hoare rules―an example = 93
  6.7 Further reading = 96
7 Completeness of the Hoare rules = 99
  7.1 G o ·· del's Incompleteness Theorem = 99
  7.2 Weakest preconditions and expressiveness = 100
  7.3 Proof of G o ·· del's Theorem = 110
  7.4 Verification conditions = 112
  7.5 Predicate transformers = 115
  7.6 Further reading = 117
8 Introduction to domain theory = 119
  8.1 Basic definitions = 119
  8.2 Streams ―an example = 121
  8.3 Constructions on cpo's = 123
    8.3.1 Discrete cpo's = 124
    8.3.2 Finite products = 125
    8.3.3 Function space = 128
    8.3.4 Lifting = 131
    8.3.5 Sums = 133
  8.4 A metalanguage = 135
  8.5 Further reading = 139
9 Recursion equations = 141
  9.1 The language REC = 141
  9.2 Operational semantics of call-by-value = 143
  9.3 Denotational semantics of call-by-value = 144
  9.4 Equivalence of semantics for call-by-value = 149
  9.5 Operational semantics of call-by-name = 153
  9.6 Denotational semantics of call-by-name = 154
  9.7 Equivalence of semantics for call-by-name = 157
  9.8 Local declarations = 161
  9.9 Further reading = 162
10 Techniques for recursion = 163
  10.1 Bekic's Theorem = 163
  10.2 Fixed-point induction = 166
  10.3 Well-founded induction = 174
  10.4 Well-founded induction = 176
  10.5 An exercise = 179
  10.6 Further reading = 181
11 Languages with higher types = 183
  11.1 An eager language = 183
  11.2 Eager operational semantics = 186
  11.3 Eager denotational semantics = 188
  11.4 Agreement of eager semantics = 190
  11.5 A lazy language = 200
  11.6 Lazy operational semantics = 201
  11.7 Lazy denotational semantics = 203
  11.8 Agreements of lazy semantics = 204
  11.9 Fixed-point operators = 209
  11.10 Observations and full abstraction = 215
  11.11 Sums = 219
  11.12 Further reading = 221
12 Information systems = 223
  12.1 Recursive types = 223
  12.2 Information systems = 225
  12.3 Closed families and Scott predomains = 228
  12.4 A cpo of information systems = 233
  12.5 Constructions = 236
    12.5.1 Lifting = 237
    12.5.2 Sums = 239
    12.5.3 Product = 241
    12.5.4 Lifted function space 243
  12.6 Further reading = 249
13 Recursive types = 251
  13.1 An eager language = 251
  13.2 Eager operational semantics = 255
  13.3 Eager denotational semantics = 257
  13.4 Adequacy of eager semantics = 262
  13.5 The eager λ-calculus = 267
  13.6 A lazy language = 278
  13.7 Lazy operational semantics = 278
  13.8 Lazy denotational semantics = 281
  13.9 Adequacy of lazy semantics = 288
  13.10 The lazy λ-calculus = 290
    13.10.1 Equational theory = 291
    13.10.2 A fixed-point operator = 292
  13.11 Further reading = 295
14 Nondeterminism and parallelism = 297
  14.1 Introduction = 297
  14.2 Guarded commands = 298
  14.3 Communication processes = 303
  14.4 Milner's CCS = 308
  14.5 Pure CCS = 311
  14.6 A specification language = 316
  14.7 The modal ν- calculus = 321
  14.8 Local modal checking = 327
  14.9 Further reading = 335
A Incompleteness and undecidability = 337
Bibliography = 353
Index = 357