ACTION SEMANTICS PETER D. MOSSES Department of Computer Science Aarhus University, Denmark CAMBRIDGE UNIVERSITY PRESS http://www.cambridge.org © Cambridge University Press 1992 First published 1992 First paperback edition 2005 ISBN 0 521 40347 2 hardback ISBN 0 521 61933 5 paperback Contents I Introduction 1 1 Language Descriptions 3 1.1 Motivation 3 1.2 Requirements 4 1.3 Features 6 1.4 Syntax 8 1.4.1 Concrete Syntax 8 1.4.2 Abstract Syntax 10 1.4.3 Context-Sensitive Syntax 11 1.5 Semantics 13 1.5.1 Semantic Functions 13 1.5.2 Semantic Entities 15 1.6 Pragmatics 18 2 Action Semantic Descriptions 21 2.1 Abstract Syntax 24 2.2 Semantic Functions 27 2.3 Semantic Entities 31 3 Algebraic Specifications 36 3.1 A Natural Example 39 3.1.1 Symbols 41 3.1.2 Axioms 42 3.1.3 Models 47 3.2 Grammars 50 3.3 Semantic Equations 51 3.4 Structural Operational Semantics 52 VI II Action Notation 57 4 Basic 59 4.1 Actions 62 4.2 /Action Notation/Facets 63 5 Data 67 5.1 /Data Notation 71 5.1.1 General 71 5.1.2 Instant 71 5.1.3 Tuples 72 5.1.4 Truth-Values 74 5.1.5 Numbers 75 5.1.6 Characters 78 5.1.7 Lists/Flat 79 5.1.8 Lists/Nested 80 5.1.9 Strings 81 5.1.10 Syntax 81 5.1.11 Sets 82 5.1.12 Maps 83 5.2 /Action Notation/Basic/Data 84 6 Functional 88 6.1 Actions 90 6.2 Yielders 92 6.3 /Action Notation/Basic/Yielders 93 6.4 /Action Notation/Facets 94 7 Declarative 98 7.1 Actions 102 7.2 Yielders 104 7.3 Data 105 7.4 /Action Notation/Facets 105 8 Imperative 108 8.1 Actions 110 8.2 Yielders 110 8.3 Data Ill 8.4 /Action Notation/Facets Ill Vll 9 Reflective 114 9.1 Actions 116 9.2 Yielders 117 9.3 Data 117 10 Communicative 120 10.1 Actions 123 10.2 Yielders 125 10.3 Data 125 10.4 /Action Notation/Facets 126 III Semantic Descriptions 129 11 Statements 131 11.1 /Ad/Abstract Syntax 132 11.2 /Ad/Semantic Functions 133 11.2.1 Statements 133 11.3 /Ad/Semantic Entities 134 12 Literals 136 12.1 /Ad/Abstract Syntax 137 12.2 /Ad/Semantic Functions 138 12.2.1 Literals 138 12.3 /Ad/Semantic Entities 139 12.3.1 Sorts 139 12.3.2 Values 139 12.3.3 Numbers 139 12.3.4 Characters 140 12.3.5 Arrays 140 13 Expressions 142 13.1 /Ad/Abstract Syntax 144 13.2 /Ad/Semantic Functions 145 13.2.1 Expressions 145 13.2.2 Statements 148 13.3 /Ad/Semantic Entities 149 13.3.1 Values 149 13.3.2 Numbers 149 13.3.3 Arrays 150 vm 14 Declarations 152 14.1 /Ad/Abstract Syntax 154 14.2 /Ad/Semantic Functions 156 14.2.1 Declarations 156 14.2.2 Statements 157 14.2.3 Expressions 157 14.2.4 Identifiers 159 14.3 /Ad/Semantic Entities 159 14.3.1 Sorts 160 14.3.2 Values 160 14.3.3 Arrays 160 14.3.4 Records 160 14.3.5 Packages 160 15 Variables 163 15.1 /Ad/Abstract Syntax 167 15.2 /Ad/Semantic Functions 168 15.2.1 Declarations 168 15.2.2 Types 169 15.2.3 Statements 171 15.2.4 Expressions 171 15.3 /Ad/Semantic Entities 173 15.3.1 Sorts 173 15.3.2 Values 173 15.3.3 Variables 173 15.3.4 Types 173 15.3.5 Accesses 174 15.3.6 Arrays 174 15.3.7 Records 174 16 Subprograms 177 16.1 /Ad/Abstract Syntax 181 16.2 /Ad/Semantic Functions 182 16.2.1 Declarations 182 16.2.2 Statements 185 16.2.3 Expressions 187 16.3 /Ad/Semantic Entities 190 16.3.1 Sorts 190 16.3.2 Subprograms 191 16.3.3 Escapes 192 16.3.4 Errors 192 IX 17 Tasks 195 17.1 /Ad/Abstract Syntax 197 17.2 /Ad/Semantic Functions 198 17.2.1 Programs 198 17.2.2 Declarations 199 17.2.3 Statements 200 17.3 /Ad/Semantic Entities 202 17.3.1 Sorts 202 17.3.2 Tasks 203 17.3.3 Alternatives 203 17.3.4 Required Bindings 203 IV Conclusion 205 18 Other Frameworks 207 18.1 Denotational Semantics 208 18.2 VDM 211 18.3 Initial Algebra Semantics 212 18.4 Algebraic Semantics 212 18.5 Abstract Semantic Algebras 213 18.6 First-Order Identities 213 18.7 Evolving Algebras 214 18.8 Structural Operational Semantics 214 18.9 Hoare Logic 215 18.10Weakest Preconditions 216 19 Development 217 19.1 Origins 218 19.2 Current Status 225 19.3 Projects 228 19.4 Mailing List 228 Appendices 230 A AD Action Semantics 231 A.I Abstract Syntax 233 A.2 Semantic Functions 235 A.2.1 Identifiers 235 A.2.2 Literals 235 A.2.3 Expressions 235 A.2.4 Statements 241 A.2.5 Declarations 244 A.2.6 Types 248 A.2.7 Programs 249 A.3 Semantic Entities 250 A.3.1 Sorts 250 A.3.2 Values 250 A.3.3 Variables 250 A.3.4 Types 251 A.3.5 Numbers 251 A.3.6 Characters 252 A.3.7 Accesses 252 A.3.8 Arrays 253 A.3.9 Records 255 A.3.10 Packages 256 A.3.11 Subprograms 257 A.3.12 Tasks 259 A.3.13 Alternatives 260 A.3.14 Escapes 260 A.3.15 Errors 260 A.3.16 Required Bindings 260 B Action Notation 261 B.I Basic 263 B.2 Functional 264 B.3 Declarative 265 B.4 Imperative 266 B.5 Reflective 268 B.6 Communicative 268 B.7 Directive 270 B.8 Hybrid 271 B.9 Facets 272 XI C Operational Semantics 278 C.I Abstract Syntax 280 C.I.I Actions 280 C.1.2 Yielders 280 C.1.3 Data 281 C.2 Semantic Entities 281 C.2.1 Acting 281 C.2.2 States 282 C.2.3 Commitments 282 C.2.4 Processing 283 C.3 Semantic Functions 284 C.3.1 Data 284 C.3.2 Yielders 284 C.3.3 Actions 285 C.3.4 Processes 291 C.4 Equivalence 293 C.4.1 Bisimulation 293 C.4.2 Testing Equivalence 295 D Informal Summary 296 D.I Basic Action Notation 299 D.2 Functional Action Notation 301 D.3 Declarative Action Notation 303 D.4 Imperative Action Notation 305 D.5 Reflective Action Notation 307 D.6 Communicative Action Notation 308 D.7 Directive Action Notation 311 D.8 Hybrid Action Notation 313 D.9 Facets 314 Xll E Data Notation 316 E.I Instant 318 E.2 Tuples 319 E.3 Truth-Values 321 E.4 Numbers 322 E.4.1 Naturals 322 E.4.2 Integers 324 E.4.3 Rationals 325 E.4.4 Approximations 327 E.5 Characters 327 E.6 Lists 329 E.6.1 Flat 329 E.6.2 Nested 330 E.7 Strings 331 E.8 Syntax 332 E.9 Sets 332 E.10 Maps 334 F Meta-Notation 336 F.I Informal Summary 336 F.I.I Vocabulary 337 F.1.2 Sentences 338 F.1.3 Specifications 340 F.2 Formal Abbreviations 341 F.2.1 Specifications 341 F.2.2 Sentences 342 F.3 Abstract Syntax 345 F.4 Logic 346 G Assessment 347 G.I Modula-3 348 G.2 Ada 348 G.3 A Functional Programming Language 349 Bibliography 350 Symbol Index 357 Concept Index 365