Formal Aspects of Computing, Volume 4

Volume 4, Number 1, 1992

C. A. Middelburg: Modular Structuring of VDM Specifications in VVSL. 13-47
Chris George: The NDB Database Specified in the RAISE Specification Language. 48-75
Ian J. Hayes: VDM and Z: A Comparative Case Study. 76-99 , further work
Edmund Kazmierczak: Modularising the Specification of a Small Database System in Extended ML. 100-142

Parosh Aziz Abdulla: Automatic Verification of a Class Systolic Circuits. 149-194
Johan J. Lukkien, Jan L. A. van de Snepscheut: Weakest Preconditions for Progress. 195-236

José Luiz Fiadeiro, T. S. E. Maibaum: Temporal Theories as Modularisation Units for Concurrent System Specification. 239-272
James H. Anderson, Mohamed G. Gouda: A Criterion for Atomicity. 273-298
Michael Fisher: A Model Checker for Linear Time Temporal Logic. 299-319

Olaf Owe: Axiomatic Treatment of Processes with shared Variables Revisited. 323-340 , further work
Heinz Faßbender, Heiko Vogler: An Implementation of Syntax Directed Functional Programming on Nested-Stack Machines. 341-375
Pierre America, Jan J. M. M. Rutten: A Layered Semantics for a Parallel Object-Oriented Language. 376-408

Lambert G. L. T. Meertens: Paramorphisms. 413-424
Jonathan P. Seldin: Coquand's Calculus of Constructions: A Mathematical Foundation for a Proof Development System. 425-441 , further work
Zhiming Liu, Mathai Joseph: Transformation of Programs for Fault-Tolerance. 442-469 , further work
J. Roger Hindley: Types with Intersection: An Introduction. 470-486 , further work
Andrew Kay, Peter Lupton: Sequential to Parallel Buffer Refinement (Short Communication). 487-492

Fredrik Orava, Joachim Parrow: An Algebraic Verification of a Mobile Network. 497-543
Noureddine Boudriga, Fathi Elloumi, Ali Mili: On the Lattice of Specifications: Applications to a Specification Methodology. 544-571
Eike Best, Ludmila Cherkasova, Jörg Desel: Compositional Generation of Home States in Free Choice Nets. 572-581
Nissim Francez, Ralph-Johan Back, Reino Kurki-Suonio: On Equivalence-Completions of Fairness Assumtions. 582-591

David M. Russinoff: A Verification System for Current Programs Based on the Boyer-Moore Prover. 597-611
Lucia Pomello, Carla Simone: An Algebraic Characterisation of Elementary Net System (Observable) State Space. 612-637
José L. Balcázar, Joaquim Gabarró, Miklos Santha: Deciding Bisimilarity is P-Complete. 638-648
M. W. Shields: Multitraces, Hypertraces and Partial Order Semantics. 649-672
Maarten M. Fokkinga: Calculate Categorically! 673-692
C. T. P. Burton: Program Morphisms. 693-726
Masaaki Mizuno, David A. Schmidt: A Security Flow Control Algorithm and Its Denotational Semantics Correctness Proof. 727-754
William R. Bevier, William D. Young: Machine Checked Proofs of the Design of a Fault-Tolerance Circuit. 755-775
Jeroen Fokker: The Systematic Construction of a One-Combinator Basis for Lambda-Terms. 776-780