Оглавление
Therese Hardin. Concepts and Semantics of Programming Languages 1
Table of Contents
List of Illustrations
List of Tables
Guide
Pages
Concepts and Semantics of Programming Languages 1. A Semantical Approach with OCaml and Python
Foreword
Preface
1. From Hardware to Software
1.1. Computers: a low-level view
1.1.1. Information processing
1.1.2. Memories
1.1.3. CPUs
1.1.4. Peripheral devices
1.2. Computers: a high-level view
1.2.1. Modeling computations
1.2.2. High-level languages
1.2.3. From source code to executable programs
1.2.3.1. Lexical analysis
1.2.3.2. Syntactic analysis
1.2.3.3. Semantic analyses
1.2.3.4. Code interpretation/generation
1.2.3.5. Linking
1.2.3.6. Interpretation and virtual machines
2. Introduction to Semantics of Programming Languages
2.1. Environment, memory and state. 2.1.1. Evaluation environment
2.1.2. Memory
2.1.3. State
2.2. Evaluation of expressions
2.2.1. Syntax
2.2.2. Values
2.2.3. Evaluation semantics
2.3. Definition and assignment. 2.3.1. Defining an identifier
2.3.2. Assignment
2.4. Exercises
3. Semantics of Functional Features
3.1. Syntactic aspects. 3.1.1. Syntax of a functional kernel
3.1.2. Abstract syntax tree
3.1.3. Reasoning by induction over expressions
Box 3.1.Structural induction scheme over e ∈ Exp2
3.1.4. Declaration of variables, bound and free variables
3.2. Execution semantics: evaluation functions
3.2.1. Evaluation errors
3.2.2. Values
3.2.3. Interpretation of operators
3.2.4. Closures
3.2.5. Evaluation of expressions
3.2.5.1. Order of evaluation of subexpressions
3.2.5.2. Lexical and dynamic scope
3.3. Execution semantics: operational semantics
3.3.1. Simple expressions
Box 3.2.Operational semantics of simple expressions inExp2
3.3.2. Call-by-value
Box 3.3.Operational semantics ofExp2: call-by-value
3.3.3. Recursive and mutually recursive functions
3.3.4. Call-by-name
Box 3.4.Operational semantics ofExp2: call-by-name
3.3.5. Call-by-value versus call-by-name
3.4. Evaluation functions versus evaluation relations
3.4.1. Status of the evaluation function
3.4.2. Induction over evaluation trees
3.5. Semantic properties
3.5.1. Equivalent expressions
3.5.2. Equivalent environments
3.6. Exercises
Box 3.5.Small-step operational semantics
4. Semantics of Imperative Features
4.1. Syntax of a kernel of an imperative language
4.2. Evaluation of expressions
4.3. Evaluation of definitions
Box 4.1.Example: execution of a sequence of definitions
4.4. Operational semantics
4.4.1. Big-step semantics
Box 4.2.Big-step operational semantics of Lang3
4.4.2. Small-step semantics
Box 4.3.Small-step operational semantics of Lang3
4.4.3. Expressiveness of operational semantics
4.5. Semantic properties
4.5.1. Equivalent programs
4.5.2. Program termination
4.5.3. Determinism of program execution
Box 4.4.Reasoning scheme by structural induction over 〈Mem, c〉 ↠Env Mem′
4.5.4. Big steps versus small steps
4.6. Procedures
4.6.1. Blocks
4.6.2. Procedures. 4.6.2.1. Language of definitions
4.6.2.2. Procedure call mechanisms. 4.6.2.2.1. Call by value
Box 4.6.Big-step operational semantics: calls to a procedure
4.6.2.2.2. Call by reference
4.7. Other approaches
4.7.1. Denotational semantics. 4.7.1.1. Partial functions associated with a program
Box 4.7.Denotational semantics
4.7.1.2. Existence, uniqueness and computation of the least fixpoint of a functional. 4.7.1.2.1. Partial order over partial functions
4.7.1.2.2. Complete partial orders
4.7.1.2.3. Continuous functions
4.7.1.2.4. Least fixpoint of a continuous function over a ccpo
4.7.1.2.5. Example
4.7.2. Axiomatic semantics, Hoare logic
4.7.2.1. Partial correctness. 4.7.2.1.1. Provable Hoare triples
4.7.2.1.2. Validity and completeness
4.7.2.2. Total correctness
4.8. Exercises
5. Types
5.1. Type checking: when and how?
5.1.1. When to verify types?
5.1.2. How to verify types?
5.2. Informal typing of a program Exp2. 5.2.1. A first example
5.2.2. Typing a conditional expression
5.2.3. Typing without type constraints
5.2.4. Polymorphism
5.3. Typing rules in Exp2
5.3.1. Types, type schemes and typing environments
5.3.2. Generalization, substitution and instantiation
5.3.3. Typing rules and typing trees
5.4. Type inference algorithm in Exp2
5.4.1. Principal type
5.4.2. Sets of constraints and unification
Box 5.2.Type unification algorithm for Exp2
5.4.3. Type inference algorithm. 5.4.3.1. Instantiation of type schemes
5.4.3.2. Composition of substitutions
5.4.3.3. Type inference
Box 5.3.Type inference algorithm for Exp2
5.5. Properties. 5.5.1. Properties of typechecking
5.5.2. Properties of the inference algorithm
5.6. Typechecking of imperative constructs
5.6.1. Type algebra
5.6.2. Typing rules
Box 5.4.Typing rules for expressions inLang3
5.6.3. Typing polymorphic definitions
5.7. Subtyping and overloading
5.7.1. Subtyping
Box 5.7.Subtyping rules
5.7.2. Overloading
6. Data Types. 6.1. Basic types
6.1.1. Booleans
6.1.2. Integers
6.1.2.1. Size of integers
6.1.2.2. Signed and unsigned integers
6.1.2.3. Overflow
6.1.2.4. Mixing integers
6.1.2.5. Integer arithmetic
6.1.2.6. Implicit conversion of integers in C
6.1.3. Characters
6.1.4. Floating point numbers
6.1.4.1. Mixing integers and floating point numbers
6.2. Arrays
6.3. Strings
6.4. Type definitions
6.4.1. Type abbreviations
6.4.2. Records
6.4.3. Enumerated types
6.4.4. Sum types
6.4.4.1. Typing sum types
6.5. Generalized conditional
6.5.1. C styleswitch/case
6.5.2. Pattern matching
6.5.2.1. ML style pattern matching: formalization
6.5.2.1.1. Order of patterns
6.5.2.1.2. Operational semantics
6.5.2.1.3. Typing rules
6.5.2.2. Extensions and other forms of matching. 6.5.2.2.1. Guarded patterns
6.5.2.2.3. Matching records
6.6. Equality
6.6.1. Physical equality
6.6.2. Structural equality
6.6.3. Equality between functions
7. Pointers and Memory Management
7.1. Addresses and pointers
7.2. Endianness
7.3. Pointers and arrays
7.4. Passing parameters by address
7.5. References
7.5.1. References in C++
7.5.2. References in Java
7.6. Memory management
7.6.1. Memory allocation
7.6.1.1. Dynamic allocation
7.6.1.2. Allocation for large structures
7.6.1.3. Dynamic allocation operators
7.6.2. Freeing memory
7.6.3. Automatic memory management
7.6.3.1. Reference counting GC
7.6.3.2. Mark-and-sweep GC
7.6.3.3. Copying GC
7.6.3.4. Generational GC
7.6.3.5. Conservative GC
8. Exceptions. 8.1. Errors: notification and propagation
8.1.1. Global variable
8.1.2. Record definition
8.1.3. Passing by address
8.1.4. Introducing exceptions
8.2. A simple formalization: ML-style exceptions
8.2.1. Abstract syntax
8.2.2. Values
8.2.3. Type algebra
8.2.4. Operational semantics
8.2.5. Typing
8.3. Exceptions in other languages
8.3.1. Exceptions in OCaml
8.3.2. Exceptions in Python
8.3.3. Exceptions in Java
8.3.4. Exceptions in C++
Conclusion
Appendix. Solutions to the Exercises
List of Notations
Index of Programs
References
Index
WILEY END USER LICENSE AGREEMENT
