Denotational Semantics pdf epub mobi txt 電子書 下載2025

想要找書就要到 小美書屋

立刻按 ctrl+D收藏本頁

你會得到大驚喜!!

Denotational semantics is a methodology for giving mathematical meaning to programming languages and systems. It was developed by Christopher Strachey’s Programming Research Group at Oxford University in the 1960s. The method combines mathematical rigor, due to the work of Dana Scott, with notational elegance, due to Strachey. Originally used as an analysis tool, denotational semantics has grown in use as a tool for language design and implementation.

This book was written to make denotational semantics accessible to a wider audience and to update existing texts in the area. I have presented the topic from an engineering viewpoint, emphasizing the descriptional and implementational aspects. The relevant mathematics is also included, for it gives rigor and validity to the method and provides a foundation for further research.

The book is intended as a tutorial for computing professionals and as a text for university courses at the upper undergraduate or beginning graduate level. The reader should be acquainted with discrete structures and one or more general purpose programming languages. Experience with an applicative-style language such as LISP, ML, or Scheme is also helpful.

Dave Schmidt

Professor Emeritus

Ph.D. 1981, Kansas State University

Post-doctoral fellow, 1982-83, Edinburgh University

Visiting Positions:

École Polytechnique, Palaiseau, 2003-04

IRISA, Rennes, France, 2004

École Normale Superieure d'Ulm, Paris, 1998 and 2006

Aarhus University, Denmark, 1997

University of Glasgow, Scotland, 1989 and 1995

University of Copenhagen, Denmark, 1987 and 1993

Edinburgh University, Scotland, 1991 and 1992

Research

Static analysis, abstract interpretation, denotational semantics.

Selected Publications

Schmidt, D.A. The Structure of Typed Programming Languages. MIT Press, Cambridge, MA, 367 pages, 1994.

Schmidt, D.A. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Inc., Boston, MA, 331 pages, 1986.

See also http://people.cis.ksu.edu/~schmidt/papers/home.html

Preface
Chapter 0 INTRODUCTION
Methods for Semantics Specification
Suggested Readings
Chapter 1 SYNTAX
1.1 Abstract Syntax Definitions
1.2 Mathematical and Structural Induction
Suggested Readings
Exercises
Chapter 2 SETS, FUNCTIONS, AND DOMAINS
2.1 Sets
2.1.1 Constructions on Sets
2.2 Functions
2.2.1 Representing Functions as Sets
2.2.2 Representing Functions as Equations
2.3 Semantic Domains
2.3.1 Semantic Algebras
Suggested Readings
Exercises
Chapter 3 DOMAIN THEORY I: SEMANTIC ALGEBRAS
3.1 Primitive Domains
3.2 Compound Domains
3.2.1 Product
3.2.2 Disjoint Union
3.2.3 Function Space
3.2.4 Lifted Domains and Strictness
3.3 Recursive Function Definitions
3.4 Recursive Domain Definitions
3.5 Summary
Suggested Readings
Exercises
Chapter 4 BASIC STRUCTURE OF DENOTATIONAL DEFINITIONS
4.1 The Valuation Function
4.2 Format of a Denotational Definition
4.3 A Calculator Language
Suggested Readings
Exercises
Chapter 5 IMPERATIVE LANGUAGES
5.1 A Language with Assignment
5.1.1 Programs are Functions
5.2 An Interactive File Editor
5.2.1 Interactive Input and Partial Syntax
5.3 A Dynamically Typed Language with Input and Output
5.4 Altering the Properties of Stores
5.4.1 Delayed Evaluation
5.4.2 Retaining Multiple Stores
5.4.3 Noncommunicating Commands
Suggested Readings
Exercises
Chapter 6 DOMAIN THEORY II: RECURSIVELY DEFINED FUNCTIONS
6.1 Some Recursively Defined Functions
6.2 Partial Orderings
6.3 Continuous Functions
6.4 Least Fixed Points
6.5 Domains are Cpos
6.6 Examples
6.6.1 Factorial Function
6.6.2 Copyout Function
6.6.3 Double Recursion
6.6.4 Simultaneous Definitions
6.6.5 The While-Loop
6.6.6 Soundness of Hoare’s Logic
6.7 Reasoning about Least Fixed Points
Suggested Readings
Exercises
Chapter 7 LANGUAGES WITH CONTEXTS
7.1 A Block-Structured Language
7.1.1 Stack-Managed Storage
7.1.2 The Meanings of Identifiers
7.2 An Applicative Language
7.2.1 Scoping Rules
7.2.2 Self-Application
7.2.3 Recursive Declarations
7.3 Compound Data Structures
Suggested Readings
Exercises
Chapter 8 ABSTRACTION, CORRESPONDENCE, AND QUALIFICATION
8.1 Abstraction
8.1.1 Recursive Bindings
8.2 Parameterization
8.2.1 Polymorphism and Typing
8.3 Correspondence
8.4 Qualification
8.5 Orthogonality
Suggested Readings
Exercises
Chapter 9 CONTROL AS A SEMANTIC DOMAIN
9.1 Continuations
9.1.1 Other Levels of Continuations
9.2 Exception Mechanisms
9.3 Backtracking Mechanisms
9.4 Coroutine Mechanisms
9.5 Unrestricted Branching Mechanisms
9.6 The Relationship between Direct and Continuation Semantics
Suggested Readings
Exercises
Chapter 10 IMPLEMENTATION OF DENOTATIONAL DEFINITIONS
10.1 A General Method of Implementation
10.1.1 The SIS and SPS Systems
10.2 Static Semantics Processing
10.3 The Structure of the Evaluator
10.3.1 A Stack-Based Evaluator
10.3.2 PSP and Appel’s System
10.4 Combinator-Based Semantic Notations
10.4.1 The Plumb and CERES Systems
10.5 Transformations on the Semantic Definition
10.5.1 First-Order Data Objects
10.5.2 Global Variables
10.5.3 Control Structures
10.6 Implementation of Continuation-Based Definitions
10.6.1 The CGP and VDM Methods
10.7 Correctness of Implementation and Full Abstraction
Suggested Readings
Exercises
Chapter 11 DOMAIN THEORY III: RECURSIVE DOMAIN SPECIFICATIONS
11.1 Reflexive Domains Have Infinite Elements
11.2 The Inverse Limit Construction
11.3 Applications
11.3.1 Linear Lists
11.3.2 Self-Applicative Procedures
11.3.3 Recursive Record Structures
Suggested Readings
Exercises
Chapter 12 NONDETERMINISM AND CONCURRENCY
12.1 Powerdomains
12.2 The Guarded Command Language
12.3 Concurrency and Resumption Semantics
12.4 An Alternative Semantics for Concurrency
12.5 The Powerdomain Structure
12.5.1 Discrete Powerdomains
12.5.2 General Powerdomains
Suggested Readings
Exercises
Bibliography
· · · · · · (收起)