Transitions and Trees : an Introduction to Structural Operational Semantics.

Cover; Transitions and Trees; Title; Copyright; Contents; Preface; About this book; Related work; What you need to know in advance; Ways through the book; Problems and thoughts; Related resources; Acknowledgements; About the illustrations; Illustrations; Tables; PART I: BACKGROUND; 1 A question of semantics; 1.1 Semantics is the study of meaning; 1.2 Examples from the history of programming languages; 1.2.1 ALGOL 60; 1.2.2 Pascal; 1.3 Different approaches to program semantics; 1.4 Applications of program semantics; 1.4.1 Standards for implementation.

1.4.2 Generating interpreters and compilers1.4.3 Verification and debugging -- lessons learned; The Mars Climate Orbiter; Software verification methods and tools; 1.4.4 The principles of programming languages; 2 Mathematical preliminaries; 2.1 Mathematical induction; 2.2 Logical notation; 2.2.1 Boolean connectives; 2.2.2 Quantifiers; 2.3 Sets; 2.4 Operations on sets; 2.4.1 Union; 2.4.2 Intersection; 2.4.3 Power set; 2.4.4 Cartesian product; 2.5 Relations; 2.6 Functions; 2.6.1 Partial and total functions; 2.6.2 Defining functions; 2.6.3 Function spaces; PART II: FIRST EXAMPLES.

3 The basic principles3.1 Abstract syntax; 3.1.1 The language Bims and its abstract syntax; 3.1.2 Some useful conventions; 3.2 Transition systems; 3.3 Big-step vs. small-step semantics; 3.4 Operational semantics of arithmetic expressions; 3.4.1 A big-step semantics of Aexp; Defining a structural operational semantics; How to build a derivation tree; 3.4.2 A small-step semantics of Aexp; 3.5 Proving properties; 3.5.1 Determinacy; 3.6 A semantics of Boolean expressions; 3.7 The elements of an operational semantics; 4 Basic imperative statements; 4.1 Program states.

4.1.1 A new big-step operational semantics of Aexp4.1.2 A new big-step operational semantics of Bexp; 4.2 A big-step semantics of statements; 4.2.1 The transition system for Stm; 4.2.2 On building derivation trees; A large example; Termination in the big-step semantics; 4.3 A small-step semantics of statements in Bims; 4.4 Equivalence of the two semantics; 4.5 Two important proof techniques; PART III: LANGUAGE CONSTRUCTS; 5 Control structures; 5.1 Some general assumptions; 5.2 Loop constructs; 5.2.1 Repeat-loops; 5.3 Semantic equivalence; 5.3.1 For-loops; 5.4 Abnormal termination.

5.5 Nondeterminism5.6 Concurrency; 6 Blocks and procedures (1); 6.1 Abstract syntax of Bip; 6.2 The environment-store model; 6.3 Arithmetic and Boolean expressions; 6.4 Declarations; 6.4.1 Declaring variables; 6.4.2 Procedure declarations; 6.5 Statements; 6.6 Scope rules; 6.6.1 Fully dynamic scope rules; 6.6.2 Mixed scope rules; 6.6.3 Fully static scope rules; 7 Parameters; 7.1 The language Bump; 7.1.1 Syntax of Bump; 7.1.2 Basic assumptions about our semantics; 7.2 Call-by-reference; 7.3 On recursive and non-recursive procedure calls; 7.4 Call-by-value; 7.5 Call-by-name.

7.5.1 The informal description of call-by-name.

A rigorous, self-contained introduction to the theory of operational semantics of programming languages and its use.

Print version record.

Includes bibliographical references and index.

English.

eBooks on EBSCOhost EBSCO eBook Subscription Academic Collection - Worldwide