Formal Aspects of Computing, Volume 7

Volume 7, Number 1, 1995

Jan L. A. van de Snepscheut: The Sliding-Window Protocol Revisited. 3-17
José Félix Costa, Amílcar Sernadas: Progress Assumption in Concurrent Systems. 18-36
Michael J. Butler, Carroll Morgan: Action Systemes, Unbounded Nondeterminism, and Infinite Traces. 37-53
Steve King, Carroll Morgan: Exits in the Refinement Calculus. 54-76
Pierre Lescanne: Termination of Rewrite Systems by Elementary Interpretations. 77-90
J. Coenen: Hoare's Logic and VDM. 91-105

Naoki Kobayashi, Akinori Yonezawa: Asynchronous Communication Model Based on Linear Logic. 113-149
J. Michael Spivey: Unification: A Case-Study in Data Refinement. 150-168
Ingrid Rewitzky, Chris Brink: Predicate Transformers as Power Operations. 169-182
Sunil Vadera: Proof by Analogy in Mural. 183-206
Bryan S. Todd, Richard Stamper: A Formal Model of Explanation. 207-225

Nancy A. Lynch, Roberto Segala: A Comparison of Simulation Techniques and Algebraic Tachniques for Verifying Concurrent Systems. 231-265
Jane Sinclair, Jim Woodcock: Event Refinement in State-Based Concurrent Systems. 266-288
Graeme Smith: A Fully Abstract Semantics of Classes for Object-Z. 289-313
Lone Leth, Bent Thomsen: Some Facile Chemistry. 314-328
Ian J. Hayes, Brendan P. Mahony: Using Units of Measurement in Formal Specifications. 329-347

Rutger M. Dijkstra: DUALITY: A Simple Formalism for the Analysis of UNITY. 353-388
Wim H. Hesselink: Safety and Progress of Recursive Procedures. 389-411
Simon J. Thompson: A Logic for Miranda, Revisited. 412-429
Ian J. Hayes, Jeff W. Sanders: Specification by Interface Separation. 430-439
Antti Valmari, Martti Tienari: Compositional Failure-based Semantics Models for Basic LOTOS. 440-468

Peter B. Ladkin, Stefan Leue: Interpreting Message Flow Graphs. 473-509
Zhiming Liu, Mathai Joseph, Tomasz Janowski: Verification of Schedulability for Real-Time Programs. 510-532
Howard Barringer, Michael Fisher, Dov M. Gabbay, Graham Gough, Richard Owens: METATEM: An Introduction. 533-549
Kai Engelhardt, Willem P. de Roever: Towards a Practitioners' Approach to Abadi and Lamport's Method. 550-575
K. Rustan M. Leino: A Method for Showing Progress. 576-580

Philippe Noël: A Transformation-Based Synthesis of Temporal Specifications. 587-619
Ian Maung: On Simulation, Subtyping and Substitutability in Sequential Object Systems. 620-651
David A. Naumann: Data Refinement, Call by Value and Higher Order Programs. 651-662
Sergei Gorlatch, Christian Lengauer: Parallelisation of Divide-and-Conquer in the Bird-Meertens Formalism. 663-682
Rajit Manohar, K. Rustan M. Leino: Conditional Composition. 683-703
Paul Mukherjee, Victoria Stavridou: A Theory pf Orwellian Specifications with NewThink. 704-727