Bücher der Reihe Formal Approaches to Computing and Information Technology (FACIT)

With contributions by numerous experts.

Rationale Software engineering aims to develop software by using approaches which en able large and complex program suites to be developed in a systematic way.

On the Refinement Calculus gives one view of the development of the refinement calculus and its attempt to bring together - among other things - Z specifications and Dijkstra's programming language. It is an excellent source of reference material for all those seeking the background and mathematical underpinnings of the refinement calculus.

Software Specification Methods provides the formal methods practitioner with a survey of the key software specification methods. This book is intended for industrial and commercial practitioners who need to expand their knowledge of software specification methods.

Industrial Strength Formal Methods in Practice provides hands-on experience and guidance for anyone who needs to apply formal methods successfully in an industrial context.

This volume presents twelve case studies that use RAISE - Rigorous Approach to Industrial Software Engineering - to construct, analyse, develop and apply formal specifications.

The Idea of Program Refinement Programs are complex. An approach, advocated for a long time, is to separate a concise specification of a program - the "what" - from a possibly involved implementation - the "how". Yet the specification of the graphical layout is secondary compared to the specification of the possible transactions.

The reader will be able to formulate problems in measurable terms, appraise and compare formal specifications, assess and enhance existing measurement practices, and devise measurement schemes for describing objective characteristics and expressing value judgements.

An overview of the use of formal object-oriented methods: it covers how and where they should be introduced into the development process, how they can be introduced selectively for critical parts of an application, and how to incorporate them effectively into existing developmental practices.

That is, the failure of the system to produce correct results could result in the loss of human life, mass destruction of property (in the form of ships and cargo) as well as financial losses and loss of competitive advantage for the shipping firm.

Notations for Software Design aims to explain formal specification and design to practitioners in software development, and to set out the ingredients of a sound software design process. It examines COLD-1, which is currently being implemented by Philips in many of its business centres. The fact that it is a wide-spectrum language which supports many styles of specification makes it an excellent basis for the volume. It also examines some widely-used informal techniques, such as Venn diagrams and Petri nets, thus creating a strong link between current and future practice. Rather than proposing new pictorial notations the authors place existing ones into a coherent framework, and explain practical ways of exploiting them in conjunction with COLD-1.

Formal methods have already been shown to improve the development process and quality assurance in system design and implementation. This volume examines whether these benefits also apply to the field of human-computer interface design and implementation, and whether formal methods can offer useful support in usability evaluation and obtaining more reliable implementations of user requirements. Its main aim is to compare the different approaches and examine which particular type of implementation and problem each one is best suited to. To enable the reader to compare and contrast the approaches as easily as possible, each one is applied to the same case study: the specification of an ideal Netscape-like web browser and html page server. The resulting volume will provide invaluable reading for final year undergraduate and postgraduate courses on user interfaces, user interface design, and applications of formal methods.