Concepts and Semantics of Programming Languages 1

Concepts and Semantics of Programming Languages 1
Автор книги: id книги: 2052342     Оценка: 0.0     Голосов: 0     Отзывы, комментарии: 0 16977,8 руб.     (184,02$) Читать книгу Купить и скачать книгу Купить бумажную книгу Электронная книга Жанр: Программы Правообладатель и/или издательство: John Wiley & Sons Limited Дата добавления в каталог КнигаЛит: ISBN: 9781119824091 Скачать фрагмент в формате   fb2   fb2.zip Возрастное ограничение: 0+ Оглавление Отрывок из книги

Реклама. ООО «ЛитРес», ИНН: 7719571260.

Описание книги

This book – the first of two volumes – explores the syntactical constructs of the most common programming languages, and sheds a mathematical light on their semantics, while also providing an accurate presentation of the material aspects that interfere with coding. <p><i>Concepts and Semantics of Programming Languages 1</i> is dedicated to functional and imperative features. Included is the formal study of the semantics of typing and execution; their acquisition is facilitated by implementation into OCaml and Python, as well as by worked examples. Data representation is considered in detail: endianness, pointers, memory management, union types and pattern-matching, etc., with examples in OCaml, C and C++. The second volume introduces a specific model for studying modular and object features and uses this model to present Ada and OCaml modules, and subsequently Java, C++, OCaml and Python classes and objects. <p>This book is intended not only for computer science students and teachers but also seasoned programmers, who will find a guide to reading reference manuals and the foundations of program verification.

Оглавление

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

Отрывок из книги

Series EditorJean-Charles Pomerol

Thérèse Hardin

.....

The first two analysis phases of compilation only concern the textual structure of the source. They do not concern the meaning of the program, i.e. its semantics. Source texts that pass the syntactic analysis phase do not always have meaning. The phrase “the sea eats a derivable rabbit” is grammatically correct, but is evidently nonsense.

The best-known semantic analysis is the typing analysis, which prohibits the combination of elements that are incompatible in nature. Thus, in the previous phase, “derivable” could be applicable to a function, but certainly not to a “rabbit”.

.....

Добавление нового отзыва

Комментарий Поле, отмеченное звёздочкой  — обязательно к заполнению

Отзывы и комментарии читателей

Нет рецензий. Будьте первым, кто напишет рецензию на книгу Concepts and Semantics of Programming Languages 1
Подняться наверх