目次

Description is our business.- Concurrent processes as objects.- The Larch approach to specification.- Formal specification in metamorphic programming.- Formalizing design spaces: Implicit invocation mechanisms.- On type checking in VDM and related consistency issues.- Combining transformation and posit-and-prove in a VDM development.- A case for structured analysis/formal design.- A model-oriented method for algebraic specifications using COLD-1 as notation.- A mechanical formalization of several fairness notions.- Specification and stepwise development of communicating systems.- Writing operational semantics in Z: A structural approach.- EZ: A system for automatic prototyping of Z specifications.- Z and high level Petri nets.- An approach to the static semantics of VDM-SL.- Behavioural extension for CSP.- Cpo's do not form a cpo, and yet recursion works.- LPF and MPL? — A logical comparison of VDM SL and COLD-K.- Tactical tools for distributing VDM specifications.- An attempt to reason about shared-state concurrency in the style of VDM.- Reasoning about VDM specifications.- On formal specification of a proof tool.- Reasoning about VDM developments using the VDM support tool in mural.- EVES: An overview.- Deriving transitivity of VDM-reification in DEVA.- Upgrading the pre- and postcondition technique.- The formal development of a secure transaction mechanism.- Formal development of a Serial Copy Management System.- Specification and refinement in an integrated database application environment.- Techniques for partial specification and specification of switching systems.- Specification of the MAA standard in VDM.- Unintrusive ways to integrate formal specifications in practice.- An overview of HP-SL.- CICS project report experiences and results from the use of Z in IBM.- A debugger for a Meta-IV-like meta-language.- An executable subset of Meta-IV with loose specification.- Using VDM within an object-oriented framework.- The integrated software development and verification system ATES.- Using RAISE — first impressions from the LaCoS applications.- A specification of a complex programming language statement.- The prospectra system.- The visual presentation of VDM specifications.- Mural and specbox.- The VDM domain compiler a VDM class library generator.- The Delft VDM-SL front-end.- Prototyping with temporal VDM a status report.- The Exspect tool.- CADiZ - Computer aided design in Z.- The HP-ST toolset.- The RAISE toolset.- The IBM Z tool.- The VDM-SL editor and consistency checker.- B-tool.- A VDM subset compiler.