Z: An Introduction to Formal Methods

ISBN-13: 9780471939733 / Angielski / Miękka / 1994 / 400 str.

Antoni Diller;Diller

Opis

Now that formal methods are seen as a necessary and beneficial theoretical tool for systems designers and programmers, this book offers a thorough and comprehensive tutorial introduction to Z taking as its starting point the practical use of this formal specification language. Case studies are used to illustrate all aspects of Z and are introduced early on in order to motivate the mathematical notations that have to be covered. Standard notation is used throughout. Many proofs are included and they are presented using the commonest format for natural deduction proofs. With exercises given and clear descriptions and explanations provided, this book is required reading for students and post-experience software engineers learning Z. Enhancements to this edition are more exercises, information on how to relate Z specifications to actual program code, and amendments so that the book is in line with the current language standards.

Spis treści

TUTORIAL.

First–Order Logic.

Set Theory.

Internal Telephone Directory.

More About Relations and Schemas.

Functions.

Sequences.

Bags.

Free Types.

METHODS OF REASONING.

Formal Proof.

Rigorous Proof.

Immanent Reasoning.

Reification and Decomposition.

Floyd–Hoare Logic.

Getting to Program Code.

CASE STUDIES.

Two Small Case Studies.

Wing′s Library Problem.

Partial Specification of a Text–Editor.

SPECIFICATION ANIMATION.

Animation Using Miranda.

REFERENCE MANUAL.

Methods of Definition.

Formal Definitions.

Rules and Obligations.

Appendices.

Bibliography.

Index.

Blurb

Z An Introduction to Formal Methods Second Edition Antoni Diller University of Birmingham Now that formal methods are seen as a necessary and beneficial theoretical tool for systems designers and programmers, this book offers a thorough and comprehensive tutorial introduction to Z taking as its starting point the practical use of this formal specification language. Case studies are used to illustrate all aspects of Z and are introduced early on in order to motivate the mathematical notations that have to be covered. Standard notation is used throughout. Many proofs are included and they are presented using the commonest format for natural deduction proofs. With exercises given and clear descriptions and explanations provided, this book is required reading for students and post–experience software engineers learning Z. Enhancements to this edition are more exercises, information on how to relate Z specifications to actual program code, and amendments so that the book is in line with the current language standards.