Algebraic Semantics of Imperative Programs Joseph A. Goguen and Grant Malcolm The MIT Press Cambridge, Massachusetts London, England Contents Series Foreword ix 0 Introduction 1 1 Background in General A l g e b r a and OBJ 11 1.1 Signatures 11 1.2 Algebras 16 1.3 Terms 17 1.4 Variables 21 1.5 Equations 24 1.6 Rewriting and Equational Deduction 29 1.6.1 Attributes of operations 1.6.2 Denotational semantics for objects 1.6.3 The Theorem of Constants 32 36 38 1.7 Importing Modules 40 1.8 Literature 43 1.9 Exercises 43 2 Stores, Variables, V a l u e s , and A s s i g n m e n t 51 2.1 Stores, Variables, and Values 51 2.1.1 OBJ's built-in inequality 55 2.2 Assignment 60 2.3 Exercises 64 3 C o m p o s i t i o n and Conditionals 67 3.1 Sequential Composition 70 3.2 Conditionals 71 3.3 Structural Induction 74 3.4 Exercises 76 4 P r o v i n g P r o g r a m Correctness 79 4.1 Example: Absolute Value 83 Contents 4.2 Example: Computing the Maximum of Two Values 86 4.3 Exercises 88 5 Iteration 91 5.1 Invariants 92 5.1.1 Example: greatest common divisor 98 5.2 Termination 102 5.3 Exercises 105 6 Arrays 109 6.1 Some Simple Examples 115 6.2 Exercises 118 6.3 Specifications and Proofs 119 6.4 Exercises 126 7 Procedures 131 7.1 Non-recursive Procedures 133 7.1.1 Procedures with no parameters 7.1.2 Procedures with var-parameters 7.1.3 Procedures with exp-parameters 133 139 144 Recursive Procedures 148 7.2.1 Procedures with no parameters 7.2.2 Procedures with var-parameters 149 156 7.3 Exercises 162 8 Some C o m p a r i s o n w i t h O t h e r A p p r o a c h e s 169 A S u m m a r y of t h e S e m a n t i c s 175 B First O r d e r Logic a n d I n d u c t i o n 185 C O r d e r Sorted A l g e b r a 203 7.2 Contents D OBJ3 Syntax 209 E Instructors' Guide 215 Bibliography 223 Index 227
© Copyright 2024 ExpyDoc
