L. Groves and S. Reeves (eds.) Formal Methods Pacific '97 , Proceedings of FMP'97, Springer-Verlag, Singapore, 1997, viii + 320 pages. ISBN: 981-3083-31-X. US$59 softcover.

Formal Methods Pacific '97 is an umbrella conference, incorporating the 6th Australasian Refinement Workshop and the 3rd New Zealand Formal Program Development Colloquium. The conference provided a forum for discussion of current research on mathematically based techniques for design and development of computer systems, especially formal and/or rigorous methods for developing executable programs from abstract specifications, tool support for formal software development, and practical experience with formal methods. Topics also include software specification and verification, hardware specification and verification, and specification and development of real-time and concurrent systems.

The refereed papers included in these proceedings present significant contributions to current research in formal software development within Australasia, along with several contributions from other parts of the world. The conference also included informal presentations describing work in progress; the abstracts for these are included.

Contents: Invited papers: Probabilistic Imperative Programming: A Rigorous Approach (K. Seidel et al.; Probablistic Data Refinement (A. McIver & C. Morgan); A Probabilistic Temporal Calculus Based on Expectations (C. Morgan & A. McIver). Completed Work: Refeered papers: Type Extension and Refinement (P. Bancroft & I. Hayes); The Refinement Calculator: Proof Support for Program Refinement (M. Butler et al.); A Modular Approach to Defining Composition Operators (S. Butler); A Semantics for Recursive Operations in Object-Z (A. Griffiths); An Algorithm for Pattern-Matching Mathematical Expressions (D. Hemer); Towards a Formal Semantic Base for the Type Models of the Unified Modeling Language (M. M. Larrondo-Petrie et al.); Compilation as Refinement (K. Lermer & C. Fidge); Version and Configuration Management of Formal Theories (P. Lindsay & O. Traynor); A Tactic Language for Ergo (A. Martin et al.); Supporting Data Refinement in a Program Refinement Tool (J. Shield et al.); The Mechanical Verification of Solid State Interlocking Geographical Data (A. Simpson et al.); Refinement of Infeasible Real-Time Programs (M. Utting & C. Fidge); A Comparison of Modularity in B and Cogito (G. Watson). Work in progress: Extended abstract.