Theoretical Computer Science, Volume 285, Issue 2, Pages 119-564 (28 August 2002), Rewriting Logic and its Applications

Preface......Page 1
Introduction......Page 3
Basic concepts......Page 4
Rewriting logic and formal methods......Page 7
Models of computation......Page 8
Semantics of programming languages......Page 10
Distributed architectures and components......Page 11
Specification and analysis of communication protocols......Page 12
Representing, mapping, and reasoning about logics......Page 13
Language implementations......Page 15
References......Page 16
Introduction......Page 37
Preliminary concepts and notations......Page 40
Rewrite rules......Page 41
Rule application......Page 42
Strategies......Page 44
Rules involving strategies in conditions......Page 48
Strategies on strategy evaluation......Page 49
Labelled and unlabelled rules......Page 50
Rewriting logic for rewrite rules with matching conditions......Page 51
Rewrite theories of strategies......Page 54
Applications......Page 61
Acknowledgements......Page 63
References......Page 64
Maude: specification and programmingin rewriting logic......Page 68
Introduction......Page 69
Membership equational logic......Page 71
Functional modules......Page 72
Example: arrays as lists of pairs......Page 76
Rewriting logic......Page 78
System modules......Page 79
Example: blocks world......Page 83
Object-oriented modules......Page 85
Module operations and parameterized programming......Page 88
Module hierarchies......Page 89
Theories......Page 90
Parameterized modules......Page 91
Views......Page 92
Module instantiation......Page 93
Reflection and metalevel computation......Page 95
The module META-LEVEL......Page 97
Representing modules......Page 98
Descent functions......Page 100
Parsing, pretty printing, and sort functions......Page 102
Extensions of META-LEVEL......Page 103
Internal strategies......Page 104
The rewrite engine......Page 109
Performance......Page 111
The MSCP parser......Page 112
Formal methodology and tools......Page 113
Mobile Maude......Page 115
CCS Syntax......Page 116
References......Page 120
Introduction......Page 125
Reflection in general logics......Page 126
Reflection in conditional rewriting logic......Page 127
Applications of rewriting logic reflection......Page 128
Reflection in general logics......Page 129
Reflective logics......Page 130
Preliminaries on -algebras, substitution, and contexts......Page 131
The rules of rewriting logic......Page 133
An equivalent proof system......Page 134
The signature of UNIVERSAL......Page 135
The representation function......Page 137
Representation of substitutions and contexts......Page 138
The rules of UNIVERSAL......Page 139
Correctness of the USC-universal theory......Page 142
A MSC-universal theory......Page 147
The rules of UNIVERSAL'......Page 148
Correctness of the MSC-universal theory......Page 150
The signature of UNIVERSAL''......Page 154
The rules of UNIVERSAL''......Page 155
Correctness of the MSC+-Universal Theory......Page 157
Acknowledgements......Page 161
References......Page 166
Introduction......Page 169
Summary of the paper......Page 173
Loose and tight denotation......Page 174
Hidden order sorted rewriting logic institution......Page 175
Operational vs. logical semantics......Page 182
Institutions......Page 183
Indexed and Grothendieck institutions......Page 185
Properties of the CafeOBJ institution......Page 186
Foundations of structured specifications......Page 188
Module imports......Page 189
Parameterisation......Page 192
Conclusions and future work......Page 195
References......Page 196
Introduction......Page 199
Some thoughts on name sharing......Page 202
On theories......Page 203
The unconditional, one-sorted rewriting logic......Page 207
At the basis of concurrency: on Petri nets......Page 209
Encoding substitution: on the lambda-calculus......Page 210
Extending the paradigm to non-cartesian structures......Page 212
The first-order calculus......Page 214
At the basis of higher-order: on the lambda-calculus......Page 215
Prefixes as boxes: on the asynchronous pi-calculus......Page 216
Flattening controls......Page 217
On algebraic tile logic......Page 220
A finite schema for non-determinism and parallelism: on CCS......Page 222
Channels as wires: on the asynchronous pi-calculus......Page 224
Stretching tiles......Page 230
An informal overview of the features......Page 232
Appendix......Page 234
References......Page 235
Introduction......Page 239
Prerequisites on rewriting logic and Maude......Page 241
Time models and real-time rewrite theories......Page 242
Time models......Page 243
Real-time rewrite theories......Page 245
A category of real-time rewrite theories......Page 247
Real-time theories internalized in rewriting logic......Page 248
Eager and lazy rules......Page 250
Time as an action on the whole system......Page 251
Timed automata......Page 253
Hybrid automata......Page 257
Timed and phase transition systems......Page 262
Object-oriented real-time systems......Page 265
Example: a single-thermostat system......Page 266
Object-oriented delta-systems......Page 268
Example: a multi-thermostat system......Page 269
Interval timed Petri nets......Page 270
Specifying ITPNs as real-time rewrite theories......Page 273
Timed rewriting logic in rewriting logic......Page 277
The mapping from TRL to real-time rewrite theories......Page 279
Non-right-linear rules......Page 280
Aging in TRL......Page 281
Concluding remarks......Page 282
References......Page 283
Introduction......Page 286
Rewriting logic and the Maude language......Page 288
The network model......Page 289
Network objects......Page 290
Network objects relationships......Page 291
Implementation of the object relationships......Page 292
The containment relationship......Page 293
Explicit group relationships......Page 296
Query messages......Page 297
Modification messages......Page 299
Reflection and the internal strategy language......Page 304
Network specification using reflection......Page 306
Strategies and rules for the reflective modification process......Page 307
Comparison of the two approaches......Page 311
Improving control by changing strategies......Page 312
Concluding remarks......Page 315
References......Page 316
Introduction......Page 319
The actor theory framework......Page 321
Actor theories informally......Page 322
Actor theory as a mathematical structure......Page 327
Operational semantics......Page 330
Interaction semantics......Page 333
Equational actor theory presentations, EAth......Page 335
A Ticker EAth......Page 337
The actor theory presented by EAth......Page 338
The rewriting logic theory associated with EAth......Page 339
Correspondence of computations and proofs for EAth......Page 340
Lifting correspondence to infinite proofs......Page 345
Examples......Page 347
Dispatcher EAth......Page 348
Switch EAth......Page 349
Combining switch and ticker EAths......Page 350
Showing equivalence......Page 351
Concurrency and composability......Page 353
Composition of configurations and proofs......Page 354
Composition of proof paths......Page 358
Conclusions and future work......Page 360
References......Page 362
Introduction......Page 364
Structure of the paper......Page 365
Relations......Page 366
The permutation lemma......Page 367
Oriented rewrite theory......Page 369
Coherence......Page 371
Local coherence......Page 374
Checking local coherence......Page 375
Examples of non-linearity......Page 376
Coherence completion......Page 377
Conditional rules......Page 378
Oriented matching......Page 379
Rewriting modulo identity......Page 381
Calculi with bound variables......Page 382
Structure of pi-calculus processes......Page 384
The reduction relation of the pi-calculus......Page 386
Addition of data types......Page 387
Example: double-way buffer......Page 388
An oriented rewriting logic theory for the sequent calculus......Page 389
Theorem proving modulo......Page 391
Conclusion......Page 392
References......Page 393
Introduction......Page 395
Related work......Page 396
Synopsis......Page 397
Functional specifications......Page 398
Object-oriented specifications......Page 399
Reflection......Page 400
Rewrite theories......Page 402
Object theories and process control......Page 403
Object theories......Page 404
Process control......Page 405
Maude implementation......Page 406
Refinement......Page 410
fOOSE extensions......Page 411
Object and interaction diagrams......Page 413
Enhanced diagrams......Page 414
Functional specifications......Page 415
Construction of a formal specification......Page 416
Proof obligations......Page 420
Enhanced diagrams......Page 421
Functional specifications......Page 423
Construction of a formal specification......Page 424
Proof obligations......Page 428
Appendix......Page 430
References......Page 434