Formal Aspects of Computing, Volume 12

Volume 12, Number 1, 2000

• Jan A. Bergstra, M. E. Loots:
  Program Algebra for Component Code. 1-17
  
• Ralph-Johan Back, Anna Mikhajlova, Joakim von Wright:
  Class Refinement as Semantics of Correct Object Substitutability. 18-40
  
• Martin von Mohrenschildt:
  Algebraic Composition of Function Tables. 41-51
  
• Antonio Cau:
  Composing and Refining Dense Temporal Logic Specifications. 52-70
  

Volume 12, Number 2, 2000

• Stephan Diehl:
  Natural Semantics-Directed Generation of Compilers and Abstract Machines. 71-99
  
• Rajeev Joshi, Jayadev Misra:
  Maximally Concurrent Programs. 100-119
  
• Stephen Paynter, James M. Armstrong, Jan Haveman:
  ADL: An Activity Description Language for Real-Time Networks. 120-144
  

Volume 12, Number 3, 2000

• Jeannette M. Wing, Jim Woodcock:
  The First World Congress on Formal Methods in the Development of Computing Systems. 145-146
  
• Heike Wehrheim:
  Data Abstraction Techniques in the Validation of CSP-OZ Specifications. 147-164
  
• Steve Schneider:
  Abstraction and Testing in CSP. 165-181
  
• Michael J. Butler:
  csp2B: A Practical Approach to Combining CSP and B. 182-198
  
• Andrew Martin:
  Relating Z and First-Order Logic. 199-209
  

Volume 12, Number 4, 2000

• B. Tim Denvir, José Nuno Oliveira, Nico Plat:
  The Cash-Point (ATM) `Problem'. 211-215
  
• Peter Gorm Larsen, Paul Mukherjee, Kim Sunesen:
  Using VDMTools to Model and Validate the Cash Dispenser Example. 216-217
  
• Anca Browne, Bernd Finkbeiner, Zohar Manna, Henny Sipma:
  The `Cash-Point' Service: A Verification Case Study Using STeP. 218-219
  
• Henning Dierks, Josef Tapken:
  Modelling and Verifying of a `Cash-Point Service' Using MOBY/PLC. 220-221
  
• Vahur Kotkas, Peep Küngas, Mait Harf:
  The Cash-Point Service in NUT. 222-224
  
• Oscar Slotosch:
  Modelling and Validation: AUTOFOCUS and Quest. 225-227
  
• Sophie Dupuy, Lydie du Bousquet:
  A Multi-formalism Approach for the Validation of UML Models. 228-230
  
• Timo Aaltonen, Pertti Kellomäki, Risto Pitkänen:
  Specifying Cash-Point with DisCo. 231-232
  
• Sylvan Dissoubray, Bernard Dion:
  Design of an Automatic Teller Machine with Esterel Studio. 233-236
  
• Richard Butterworth, Ann Blandford, David J. Duke:
  Demonstrating the Cognitive Plausibility of Interactive System Specifications. 237-259
  
• Gavin J. Doherty, José Creissac Campos, Michael D. Harrison:
  Representational Reasoning and Verification. 260-277
  
• Kaisa Sere, Marina A. Waldén:
  Data Refinement of Remote Procedures. 278-297
  
• Anthony C. J. Fox, Neal A. Harman:
  Algebraic Models of Correctness for Microprocessors. 298-312
  

Volume 12, Number 5, 2000

• Ralph-Johan Back, Joakim von Wright:
  Encoding, Decoding and Data Refinement. 313-349
  
• Rachel Cardell-Oliver:
  Conformance Tests for Real-Time Systems with Timed Automata Specifications. 350-371
  
• Mark Staples:
  Interfaces for Refining Recursion and Procedures. 372-391
  
• Chris M. N. Tofts:
  Symbolic Approaches to Probability Distributions in Process Algebra. 392-415
  

Volume 12, Number 6, 2000

• Cliff B. Jones:
  Editorial. 417
  
• Mike Holcombe:
  What are X-Machines? 418-422
  
• Robert M. Hierons, Mark Harman:
  Testing Conformance to a Quasi-Non-Deterministic Stream X-Machine. 423-442
  
• Florentin Ipate, Mike Holcombe:
  Generating Test Sets from Non-Deterministic Stream X-Machines. 443-458
  
• Marian Gheorghe:
  Generalised Stream X-Machines and Cooperating Distributed Grammar Systems. 459-472
  
• Tudor Balanescu:
  Generalised Stream X-Machines with Output Delimited Type. 473-484
  
• Anthony J. Cowling, Horia Georgescu, Cristina Vertan:
  A Structured Way to Use Channels for Communication in X-Machine Systems. 485-500