## VDM '91. Formal Software Development Methods. 4th International Symposium of VDM Europe, Noordwijkerhout, The Netherlands, October 21-25, 1991. Proceedings: Volume 1: Conference ContributionsThe proceedings of the fourth Vienna Development MethodSymposium, VDM'91, are published here in two volumes.Previous VDM symposia were held in 1987 (LNCS 252), 1988(LNCS 328), and 1990 (LNCS 428).The VDM symposia have been organized by VDM Europe, formedin 1985 as an advisory board sponsored by the Commission ofthe European Communities. The VDM Europe working groupconsisted of researchers, software engineers, andprogrammers, allinterested in promoting the industrialusage of formal methods for software development. The fourthVDM symposium presented not only VDM but also a large numberof other methods for formal software development.Volume 1 contains conference contributions. It has fourparts: contributions of invited speakers, papers, projectreports, and tools demonstration abstracts. The emphasis ison methods and calculi for development, verification andverification tools support, experiences from doingdevelopments, and the associated theoretical problems.Volume 2 contains four introductory tutorials (on LARCH,Refinement Calculus, VDM, and RAISE) and four advancedtutorials (on ABEL, PROSPECTRA, The B Method, and TheStack). They present a comprehensive account of the state oftheart. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Description Is Our Business | 1 |

Concurrent Processes as Objects | 9 |

The Larch Approach to Specification | 10 |

Formal Specification in Metamorphic Programming | 11 |

Implicit Invocation Mechanisms | 31 |

On Type Checking in VDM and Related Consistency Issues | 45 |

Combining Transformation and PositandProve in a VDM Development | 63 |

A Case for Structured Analysis Formal Design | 81 |

Specification and Refinement in an Integrated Database Application Environment | 496 |

Techniques for Partial Specification and Specification of Switching Systems | 511 |

Specification of the MAA Standard in VDM | 526 |

Unintrusive Ways to Integrate Formal Specifications in Practice | 545 |

An Overview of HPSL | 571 |

Experiences and Results from the Use of Z in IBM | 588 |

A Debugger for a MetaIVlike Metalanguage | 597 |

An Executable Subset of MetaIV with Loose Specification | 604 |

A Modeloriented Method for Algebraic Specifications Using COLD1 as Notation | 106 |

A Mechanical Formalization of Several Fairness Notions | 125 |

Specification and Stepwise Development of Communicating Systems | 149 |

A Structural Approach | 164 |

A System for Automatic Prototyping of Z Specifications | 189 |

Z and High Level Petri Nets | 204 |

An Approach to the Static Semantics of VDMSL | 220 |

Behavioural Extension for CSP | 254 |

Cpos do not form a Cpo and yet Recursion Works | 268 |

LPF and MPL𝜔 A Logical Comparison of VDM SL and COLDK | 279 |

Tactical Tools for Distributing VDM Specifications | 309 |

An Attempt to Reason About SharedState Concurrency in the Style of VDM | 324 |

Reasoning About VDM Specifications | 343 |

Formal Specification of a Proof Tool | 356 |

Reasoning About VDM Developments Using The VDM Support Tool in Mural | 371 |

An Overview | 389 |

Deriving Transitivity of VDMReification in DEVA | 406 |

Upgrading the Preand Postcondition Technique | 428 |

The Formal Development of a Secure Transaction Mechanism | 457 |

Formal Development of a Serial Copy Management System | 477 |

Using VDM within an ObjectOriented Framework | 619 |

The Integrated Software Development and Verification System Ates | 629 |

Using RAISE First Impressions from the LaCoS Applications | 645 |

A Specification of a Complex Programming Language Statement | 658 |

The PROSPECTRA System | 668 |

The Visual Presentation of VDM Specifications | 670 |

mural and SpecBox | 672 |

A VDM Class Library Generator | 675 |

The Delft VDMSL FrontEnd | 677 |

A Status Report | 681 |

The ExSpect tool | 683 |

CadizComputer Aided Design in Z | 685 |

The HPST Toolset | 687 |

The RAISE Toolset | 689 |

The IBM Z Tool | 691 |

The VDMSL Editor and Consistency Checker | 693 |

BTool | 695 |

A VDM Subset Compiler | 697 |

Index of Authors | |

### Other editions - View all

VDM '91. Formal Software Development Methods. 4th International Symposium of ... Soren Prehn,Hans Toetenel No preview available - 1991 |

VDM '91. Formal Software Development Methods. 4th International Symposium of ... Soren Prehn,Hans Toetenel No preview available - 1991 |

### Common terms and phrases

Abstract Machine algebraic algorithm application approach assertions axiom axiom schemas basic behaviour bytes checking COLD-K component Computer Science consistency constraint constructor constructs data transformer data types database defined denotes described DFDs domain editor environment example execution expression formal methods formal specification formula FUNC function definitions given HP-SL implementation implicit invocation input integrated interface interpretation introduced invariant logic modules MPLW natural numbers notation object operation operational semantics parameters partial equivalence relation partial functions Petri Nets possible postcondition precondition problem procedure programming language proof obligations proof system properties prove recursive refinement reification relation result rules satisfies schema semantics sequence software development Software Engineering sort specification language statement structure subset symbols syntax theorem theory tool transaction transition true TypeR updates variables VDM specification well-formed well-formedness predicate Z notation