tailieunhanh - The Z Notation:A Reference ManualSecond Edition

A computer is a general purpose device that can be programmed to carry out a finite set of arithmetic or logical operations. Since a sequence of operations can be readily changed, the computer can solve more than one kind of problem. | The Z Notation A Reference Manual Second Edition J. M. Spivey Programming Research Group University of Oxford Based on the work of J. R. Abrial I. J. Hayes C. A. R. Hoare He Jifeng C. C. Morgan J. W. Sanders I. H. S0rensen J. M. Spivey B. A. Sufrin This edition first published 1992 by Prentice Hall International UK Ltd Published 1998 by J. M. Spivey Oriel College Oxford OX1 4EW England J. M. Spivey 1989 1992 All rights reserved. No part of this publication may be reproduced stored in a retrieval system or transmitted in any form. or by any means electronic mechanical photocopying recording or otherwise without prior permission in writing from the publisher. For permission in all countries contact the author. Contents Preface vii 1 Tutorial Introduction 1 What is a formal specification 1 The birthday book 3 Strengthening the specification 7 From specifications to designs 10 Implementing the birthday book 11 A simple checkpointing scheme 17 2 Background 24 Objects and types 24 Sets and set types 25 Tuples and Cartesian product types 25 Bindings and schema types 26 Relations and functions 27 Properties and schemas 28 Combining properties 29 Decorations and renaming 30 Combining schemas 31 Variables and scope 34 Nested scopes 35 Schemas with global variables 36 Generic constructions 38 Partially-defined expressions 40 3 The Z Language 42 Syntactic conventions 42 Words decorations and identifiers 43 Operator symbols 43 Layout 46 Specifications 47 Basic type definitions 47