The mathematical concepts and notational conventions we know of as Z were first proposed around 1981. Its origins were in line with the objectives of the PRG - to establish a mathematical basis for program ming concepts and to verify the work by case studies with industry. Hence among early Z users some were from academic circles, with interests in the mathematical basis of programming; others came from industry and were involved with pilot projects and case studies linked with the Programming Research Group. Four years ago we had the first Z User Meeting, a fairly modest affair with representatives more or less equally divided between academia and industry. At the first meeting there were, as in this meeting, a variety of technical papers, reports of work in progress and discussions. A number of people from industry came along, either because they had begun to use Z or were curious about the new direction. In the discussion sessions at the end of the meeting, there were calls from attendees for the establishment of a more stable base for the notation, including work on its documentation and standards. Many of these requests have now been satisfied and the notation is now being proposed for standards development.

The Z notation has been developed at the Programming Research Group at the Oxford University Computing Laboratory and elsewhere for over a decade. It is now used by industry as part of the software (and hardware) development process in both Europe and the USA. It is currently undergoing BSI standardisation in the UK, and has been proposed for ISO standardisation internationally. In recent years researchers have begun to focus increasingly on the development of techniques and tools to encourage the wider application of Z and other formal methods and notations. This volume contains papers from the Seventh Annual Z User Meeting, held in London in December 1992. In contrast to previous years the meeting concentrated specifically on industrial applications of Z, and a high proportion of the participants came from an industrial background. The theme is well represented by the four invited papers. Three of these discuss ways in which formal methods are being introduced, and the fourth presents an international survey of industrial applications. It also provides a reminder of the improvements which are needed to make these methods an accepted part of software development. In addition the volume contains several submitted papers on the industrial use of Z, two of which discuss the key area of safety-critical applications. There are also a number of papers related to the recently-completed ZIP project. The papers cover all the main areas of the project including methods, tools, and the development of a Z Standard, the first publicly-available version of which was made available at the meeting. Finally the volume contains a select Z bibliography, and section on how to access information on Z through comp.specification.z, the international, computer-based USENET newsgroup. Z User Workshop, London 1992 provides an important overview of current research into industrial applications of Z, and will provide invaluable reading for researchers, postgraduate students and also potential industrial users of Z.

In ordinary mathematics, an equation can be written down which is syntactically correct, but for which no solution exists. For example, consider the equation x = x + 1 defined over the real numbers; there is no value of x which satisfies it. Similarly it is possible to specify objects using the formal specification language Z [3,4], which can not possibly exist. Such specifications are called inconsistent and can arise in a number of ways. Example 1 The following Z specification of a functionf, from integers to integers "f x : ~ 1 x ~ O· fx = x + 1 (i) "f x : ~ 1 x ~ O· fx = x + 2 (ii) is inconsistent, because axiom (i) gives f 0 = 1, while axiom (ii) gives f 0 = 2. This contradicts the fact that f was declared as a function, that is, f must have a unique result when applied to an argument. Hence no suchfexists. Furthermore, iff 0 = 1 andfO = 2 then 1 = 2 can be deduced! From 1 = 2 anything can be deduced, thus showing the danger of an inconsistent specification. Note that all examples and proofs start with the word Example or Proof and end with the symbol.1.

This volume contains papers from the Eighth Z User Meeting, to be held at the University of Cambridge from 29 - 30 June 1994. The papers cover a wide range of issues associated with Z and formal methods, with particular reference to practical application. These issues include education, standards, tool support, and interaction with other design paradigms such as consideration of real-time and object-oriented approaches to development. Among the actual topics covered are: the formal specification in Z of Defence Standard 00-56; formal specification of telephone features; specifying and interpreting class hierarchies in Z; and software quality assurance using the SAZ method. Z User Workshop, Cambridge 1994 provides an important overview of current research into industrial applications of Z, and will provide invaluable reading for researchers, postgraduate students and also potential industrial users of Z.

The Sixth Refinement Workshop took place at City University in London from 5th to 7th January 1994. The present volume includes all of the papers which were submitted and accepted for presentation, together with two papers by invited speakers. The workshops in the series have generally occurred at one year intervals but in this last case a two year period had elapsed. These workshops have established themselves as an important event in the calendar for all those who are interested in progress in the underlying theory of refinement and in the take-up by industry of the methods supported by that theory. One of the proposed themes of the sixth workshop was the reporting of successful adoption in industry of rigorous software development methods. The programme committee was perhaps slightly disappointed by the response from industry to the call in this respect. However, the recent period could be characterised as one of consolidation, when those companies which have made the decision that formal development methods are important to their business have been adopting them where appropriate and finding them to be worthwhile. On the other hand,. the difficult economic climate which exists in most parts of the developed world is perhaps not the context within which companies still dubious about the benefits are goil'\g to opt for making major changes in their working practices.

Refinement is the term used to describe systematic and formal methods of specifying hard- and software and transforming the specifications into designs and implementations. The value of formal methods in producing reliable hard- and software is widely appreciated by academics and workers in industry, despite the fact that certain research areas, such as the application to industrial-scale problems, are still in their infancy. This volume contains the papers presented at the 5th Refinement Workshop held in London, 8-10 January 1992. Its theme was the theory and practice of software specifications, which is the transformation of formal software specifications into more correct specifications, designs and codes. This has been an important area of research for the last 5 years and the workshop addressed specific issues and problems related to it. Among the topics discussed in this volume are: the role of refinement in software development, parallel designs and implementations, methods and tools for verification of critical properties, refinement and confidentiality, concurrent processes as objects, the compliance of Ada programs with Z specifications and a tactic driven refinement tool. This is the latest refinement workshop proceedings to be published in the Workshops in Computing series (the 3rd and 4th workshops having appeared in 1990 and 1991 respectively). It will be of interest to academic and industrial researchers, postgraduate students and research-oriented developers in the computer industry.

The papers in this volume were presented at the First International Workshop on Larch, held at MIT Endicott House near Boston on 13-15 July 1992. Larch is a family of formal specification languages and tools, and this workshop was a forum for those who have designed the Larch languages, built tool support for them, particularly the Larch Prover, and used them to specify and reason about software and hardware systems. The Larch Project started in 1980, led by John Guttag at MIT and James Horning, then at Xerox/Palo Alto Research Center and now at Digital Equipment Corporation/Systems Research Center (DEC/SRC). Major applications have included VLSI circuit synthesis, medical device communications, compiler development and concurrent systems based on Lamport's TLA, as well as several applications to classical theorem proving and algebraic specification. Larch supports a two-tiered approach to specifying software and hardware modules. One tier of a specification is wrillen in the Larch Shared Language (LSL). An LSL specification describes mathematical abstractions such as sets, relations, and algebras; its semantics is defined in terms of first-order theories. The second tier is written in a Larch interface language, one designed for a specific programming language. An interface specification describes the effects of individual modules, e.g. state changes, resource allocation, and exceptions; its semantics is defined in terms of first-order predicates over two states, where state is defined in terms of the programming language's notion of state. Thus, LSL is programming language independent; a Larch interface language is programming language dependent.

It is many years since Landin, Burge and others showed us how to apply higher order techniques and thus laid some foundations for modern functional programming. The advantage of higher order descriptions - that they can be very succinct and clear - has been percolating through ever since. Current research topics range from the design, implementation and use of higher order proof assistants and theorem provers, through program specification and verification, and programming language design, to its applications in hardware description and verification. The papers in this book represent the presentations made at a workshop held at Banff, Canada, September 10-14 1990 and organised by the Computer Science Department of the University of Calgary. The workshop gathered together researchers interested in applying higher order techniques to a range of problems. The workshop format had a few (but fairly long) presentations per day. This left ample time for healthy discussion and argument, many of which continued on into the small hours. With so much to choose from, the program had to be selective. This year's workshop was divided into five parts: 1. Expressing and reasoning about concurrency: Warren Burton and Ken Jackson, John Hughes, and Faron Moller. 2. Reasoning about synchronous circuits: Geraint Jones and Mary Sheeran (with a bonus on the fast Fourier transform from Geraint). 3. Reasoning about asynchronous circuits: Albert Camilleri, Jo Ebergen, and Martin Rem. 4. Categorical concepts for programming languages: Robin Cockett, Barry Jay, and Andy Pitts.

This volume results from the four-day scientific Second International East/West Database Workshop which took place 25th-28th September 1994, in Klagenfurt, Austria, continuing a series of workshops started in Kiev in 1990 (Lecture Notes in Computer Science No. 504, Springer, "Next Generation Information System Technology"). The aims of this workshop are twofold: first, to provide a forum for the presentation and in-depth discussion of scientific achievements in the field of advanced databases that will effectively improve the building and use of future information systems; second, to establish and increase communication between research communities which were formerly separated and, therefore, had only rare opportunities to interact. It should establish contacts between researchers from the East and from the West to make exchange of ideas possible and to trigger collaborations. However, it is not only political borders which change their perviousness as a result of -or giving rise to -new autonomies or new possibilities for interaction and collaboration. The same happens with the borders between scientific areas, in particular in the dynamically evolving areas of computer science. Databases and programming languages are integrated in object oriented databases, database and information retrieval technology form together the basis for modern (multimedia) information systems. Furthermore, the borders between different information systems change and allow various forms of collaboration while maintaining different degrees of autonomy. Heterogeneous and distributed databases are enabling technologies for these systems.