An Algebraic Approach to Compiler... | Buy

Investigates the design of compilers for procedural languages, based on the algebraic laws which these languages satisfy. Covers the concepts and notation of the reasoning language and procedures, recursion and parameters.

Preface

ix

Introduction

1

(16)

Motivation for a New Approach

2

(5)

The Reasoning Language

7

(4)

The Approach through Examples

11

(4)

The Formal Characterisation of Correctness

15

(2)

Background

17

(12)

Partial Orders and Lattices

18

(1)

The Lattice of Predicates

19

(1)

The Lattice of Predicate Transformers

20

(1)

Properties of Predicate Transformers

21

(1)

Some Refinement Calculi

22

(2)

Data Refinement

24

(3)

Refinement and Compilation

27

(2)

The Reasoning Language

29

(34)

Concepts and Notation

30

(2)

Skip, Abort and Miracle

32

(1)

Sequential Composition

33

(1)

Demonic Nondeterminism

34

(1)

Angelic Nondeterminism

34

(1)

The Ordering Relation

35

(1)

Unbounded Nondeterminism

36

(1)

Recursion

37

(1)

Approximate Inverses

37

(2)

Simulation

39

(2)

Assumption and Assertion

41

(1)

Guarded Command

42

(2)

Guarded Command Set

44

(1)

Conditional

44

(2)

Assignment

46

(1)

Generalised Assignment

47

(1)

Iteration

48

(3)

Static Declaration

51

(2)

Dynamic Declaration

53

(6)

The Correctness of the Basic Laws

59

(4)

A Simple Compiler

63

(26)

The Normal Form

63

(2)

Normal Form Reduction

65

(5)

The Target Machine

70

(2)

Simplification of Expressions

72

(4)

Control Elimination

76

(3)

Data Refinement

79

(7)

The Compilation Process

86

(3)

Procedures, Recursion and Parameters

89

(18)

Notation

89

(2)

Procedures

91

(2)

Recursion

93

(3)

Parametrised Programs

96

(3)

Parametrised Procedures

99

(2)

Parametrised Recursion

101

(2)

Discussion

103

(4)

Machine Support

107

(26)

OBJ3

108

(2)

Structure of the Specification

110

(2)

The Reasoning Language

112

(6)

An Example of a Proof

116

(2)

The Normal Form

118

(1)

A Compiler Prototype

119

(7)

Simplification of Expressions

119

(1)

Control Elimination

120

(1)

Data Refinement

121

(1)

Machine Instructions

122

(1)

Compiling with Theorems

123

(3)

Final Considerations

126

(7)

The Mechanisation

126

(2)

OBJ3, 20BJ and Rewriting Logic

128

(2)

Other systems

130

(3)

Conclusions

133

(12)

Related Work

135

(2)

Topics for Further Research

137

(6)

A Critical View

143

(2)

A. A SCHEME FOR COMPILING ARRAYS

145

(4)

B. PROOF OF LEMMA 5.1

149

(4)

C. SPECIFICATION AND VERIFICATION IN OBJ3

153

(24)

C.1 The Reasoning Language

153

(9)

C.1.1. Proof of Theorem 3.17.6

157

(2)

C.1.2. Proof of Theorem 3.17.7

159

(3)

C.2. The Normal Form

162

(4)

C.2.1. Proof of Lemma 4.2

163

(1)

C.2.2. Proof of Lemma 4.3

164

(1)

C.2.3. Proof of Theorem 4.4

164

(2)

C.3. Simplification of Expressions

166

(3)

C.3.1. Proof of Theorem 4.3

166

(1)

C.3.2. Proof of Theorem 4.5

167

(2)

C.4. Control Elimination

169

(1)

C.5. Data Refinement

170

(5)

C.5.1. Proof of Theorem 4.10

170

(2)

C.5.2. Proof of Theorem 4.14

172

(3)

C.6. Machine Instructions

175

(2)

Bibliography

177

(6)

Index

183

What is included with this book?

The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.

The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.