形式化方法.pdf-资料库

fu6543210-10292440-4744300845372411405.pdf-第1页.png

第1页 / 共176页

fu6543210-10292440-4744300845372411405.pdf-第2页.png

第2页 / 共176页

fu6543210-10292440-4744300845372411405.pdf-第3页.png

第3页 / 共176页

fu6543210-10292440-4744300845372411405.pdf-第4页.png

第4页 / 共176页

fu6543210-10292440-4744300845372411405.pdf-第5页.png

第5页 / 共176页

fu6543210-10292440-4744300845372411405.pdf-第6页.png

第6页 / 共176页

fu6543210-10292440-4744300845372411405.pdf-第7页.png

第7页 / 共176页

fu6543210-10292440-4744300845372411405.pdf-第8页.png

第8页 / 共176页

Macmillan Computer Science Series Consulting Editor: Professor F.H. Sumner, University of Manchester A. Abdellatif, J. Le Bihan and M. Limame, Oracle- A user's guide S.T. All worth and R.N. Zobel, Introduction to Real-time Software Design, second edition Ian 0. Angell, High-resolution Computer Graphics Using C Ian 0. Angell and Gareth Griffith, High-resolution Computer Graphics Using FORTRAN 77 Ian 0. Angell and Gareth Griffith, High-resolution Computer Graphics Using Pascal M. Azmoodeh, Abstract Data Types and Algorithms, second edition C. Bamford and P. Curran, Data Structures, Files and Databases, second edition Philip Barker, Author Languages for CAL A.N. Barrett and A.L. Mackay, Spatial Structure and the Microcomputer R.E. Berry, B.A.E. Meekings and M.D. Soren, A Book on C, second edition P. Beynon-Davies, Information Systems Development G.M. Birtwistle, Discrete Event Modelling on Simula B.G. Blundell and C.N. Daskalakis, Using and Administering an Apollo Network B.G. Blundell, C.N. Daskalakis, N.A.E. Heyes and T.P. Hopkins, An Introductory Guide to Si/var Lisco and HILO Simulators T.B. Boffey, Graph Theory in Operations Research Richard Bornat, Understanding and Writing Compilers Linda E.M. Brackenbury, Design ofVLSI Systems -A Practical Introduction Alan Bradley, Peripherals for Computer Systems G.R. Brookes and A.J. Stewart, Introduction to occam 2 on the Transputer J.K. Buckle, Software Configuration Management W.O. Burnham and A.R. Hall, Prolog Programming and Applications P.C. Capon and P.J. Jinks, Compiler Engineering Using Pascal J.C. Cluley,1nterfacing to Microprocessors J.C. Cluley, Introduction to Law Level Programming for Microprocessors Robert Cole, Computer Communications, second edition Derek Coleman, A Structured Programming Approach to Data E. Davalo and P. Nairn, Neural Networks S.M. Deen, Principles and Practice of Database Systems C. Delannoy, Turbo Pascal Programming Tim Den vir, Introduction to Discrete Mathematics for Software Engineering D. England eta/., A Sun User's Guide J.S. Rorentin, Microprogrammable Hardware A.B. Fontaine and F. Barrand, 80286 and 80386 Microprocessors J.B. Gosling, Design of Arithmetic Units for Digital Computers M.G. Hartley, M. Healey and P.G. Depledge, Mini and Microcomputer Systems J.A. Hewitt and R.J. Frank, Software Engineering in Modu/a-2- An Object-oriented Approach Roger Hutty, COBOL 85 Programming Roger Hutty, Z80 Assembly Language Programming for Students Roland N. Ibbett and Nigel P. Topham, Architecture of High Performance Computers, Volume I Roland N. Ibbett and Nigel P. Topham, Architecture of High Performance Computers, Volume II Patrick Jaulent, The 68000- Hardware and Software P. Jaulent, L. Baticle and P. Pillot, 68020-30 Microprocessors and their Coprocessors M.J. King and J.P. Pardoe, Program Design Using JSP- A Practical Introduction E.V. Krishnamurthy, Introductory Theory of Computer Science V.P. Lane, Security of Computer Based Information Systems Graham Lee, From Hardware to Software- An Introduction to Computers David Lightfoot, Formal Specification Using Z A.M. Lister and R.D. Eager, Fundamentals of Operating Systems ,fourth edition Elizabeth Lynch, Understanding SQL Tom Manns and Michael Coleman, Software Quality Assurance A. Mevel and T. Gueguen, Smal/ta/k-80 R.J. Mitchell, Microcomputer Systems Using the STE Bus R.J. Mitchell, Modula-2 Applied Y. Nishinuma and R. Espesser, UNIX- First contact Pham Thu Quang and C. Chartier-Kastler, MERISE in Practice Pim Oets, MS-DOS and PC-DOS- A Practical Guide, second edition (continued overleaf)

A.J. Pilavakis, UNIX Workshop Christian Queinnec, USP E.J. Redfern, Introduction to Pascal for Computational Mathematics Gordon Reece, Microcomputer Modelling by Finite Differences W.P. Salman, 0. Tisserand and B. Toulout, FORTH L.E. Scales, Introduction to Non-Linear Optimization Peter S. Sell, Expert Systems- A Practical Introduction A. G. Sutcliffe, Human-Computer Interface Design Colin J. Theaker and Graham R. Brookes, A Practical Course on Operating Systems, second edition M.R. Tolhurst eta/., Open Systems Interconnection A.J. Tyrrell, COBOL from Pascal M.J. Usher, Information Theory for Information Technologists B.S. Walker, Understanding Microprocessors Colin Walls, Programming Dedicated Microprocessors I.R. Wilson and A.M. Addyman, A Practical Introduction to Pascal- with BS6192, second edition Non-series Roy Anderson, Management, Information Systems and Computers 1.0. Angell, Advanced Graphics with the IBM Personal Computer J.E. Bingham and G.W.P. Davies, A Handbook of Systems Analysis, second edition J.E. Bingham and G.W.P. Davies, Planning for Data Communications B.V. Cordingley and D. Chamund, Advanced BASIC Scientific Subroutines N. Frude, A Guide to SPSS!PC+ Percy Melt, Introduction to Computing Tony Royce, COBOL- An Introduction Barry Thomas, A PostScript Cookbook

Formal Specification Using Z David Lightfoot School of Computing and Mathematical Sciences Oxford Polytechnic M MACMILLAN

©David Lightfoot 1991 All rights reserved. No reproduction, copy or transmission of this publication may be made without written permission. No paragraph of this publication may be reproduced, copied or transmitted save with written permission or in accordance with the provisions of the Copyright, Designs and Patents Act 1988, or under the terms of any licence permitting limited copying issued by the Copyright Licensing Agency, 33-4 Alfred Place, London WClE 7DP. Any person who does any unauthorised act in relation to this publication may be liable to criminal prosecution and civil claims for damages. First edition 1991 Published by MACMILLAN EDUCATION LTD Houndmills, Basingstoke, Hampshire RG21 2XS and London Companies and representatives throughout the world ISBN 978-0-333-54408-2 DOI 10.1007/978-1-349-12144-1 A catalogue record for this book is available from the British Library ISBN 978-1-349-12144-1 (eBook)

Contents Preface X 1 Introduction The need for formal specification ............................... 1 The role of mathematics .............................................. 2 Current use of mathematics ......................................... 3 Benefits and costs of formal specification ................... 4 The specification language Z ....................................... 4 Textual aspects of the Z notation ................................ 5 Exercises ...................................................................... 6 2 Sets in Z Types ........................................................................... 8 Built-in types ............................................................... 8 Basic types ................................................................ 10 Free types .................................................................. 10 Declarations ............................................................... 11 Single value from a type ............................................ 11 Sets of values ............................................................. 12 Set constants .............................................................. 12 The empty set ............................................................ 12 Operators ................................................................... 13 Set comprehension .................................................... 19 Ranges of numbers .................................................... 19 Disjoint sets ............................................................... 20 Partition ..................................................................... 20 Summary of notation ................................................. 21 v

vi 3 Formal Specification Using Z Exercises .................................................................... 22 Usin~ sets to describe a system - a s1mple example Introduction ............................................................... 23 The state ..................................................................... 23 Initial state ................................................................. 24 Operations ................................................................. 24 Enquiry operations .................................................... 26 Conclusion ................................................................ 27 Exercises .................................................................... 27 4 Logic: propositional calculus Introduction ............................................................... 28 Propositional calculus ............................................... 28 Operators ................................................................... 28 De Morgan's laws ..................................................... 31 Demonstrating laws ................................................... 31 Using laws ................................................................. 32 Example proof- exclusive-or ................................... 32 Laws about logical operators ..................................... 34 Relationship between logic and set theory ................ 35 Summary of notation ................................................. 36 Exercises .................................................................... 36 5 The example extended Full definition of boarding operation ........................ 37 A better way ............................................................... 38 Exercises .................................................................... 38 6 Schemas Schemas ..................................................................... 39 Schema calculus ........................................................ 41 Decoration of input- and output observations ........... 45 Example of schemas with input. ................................ .46 Overall structure of a Z specification document ........ 51 Summary of notation ................................................. 52 Exercises .................................................................... 54

Contents vii 7 Example of a Z specification document Introduction ............................................................... 56 The types ................................................................... 56 The state ..................................................................... 56 Initial state ................................................................. 57 Operations ................................................................. 57 Enquiry operations .................................................... 58 Dealing with errors .................................................... 59 Exercises .................................................................... 60 8 Logic: predicate calculus Introduction ............................................................... 61 Quantifiers ................................................................. 61 Further operations on schemas .................................. 64 Summary of notation ................................................. 67 Exercises .................................................................... 68 9 Relations A relation is a set ....................................................... 69 Cartesian product ....................................................... 69 Relations .................................................................... 70 Declaring a relation .................................................... 71 Maplets ...................................................................... 71 Membership ............................................................... 72 Domain and range ..................................................... 72 Relational image ........................................................ 74 Constant value for a relation ...................................... 74 Example of a relation ................................................ 75 Restriction ................................................................. 76 Example of restriction ............................................... 78 Composition ............................................................... 78 Repeated composition ............................................... 80 Example ..................................................................... 80 Identity relation .......................................................... 81 Inverse of a relation ................................................... 81 Examples ................................................................... 82 Summary of notation ................................................. 83 Exercises .................................................................... 84

资料库

形式化方法.pdf

相关推荐

课程资源

热门标签

最新资料