Read more
Informationen zum Autor STEVE SCHNEIDER is Professor of Computing in the Department of Computing, University of Surrey, UK. He has taught the B-method at undergraduate and postgraduate level over a number of years, and has published papers on B at international formal methods conferences and workshops. Klappentext This book provides a textbook introduction to the B-Method, a rigorous methodology for the development of correct software. The text covers all stages of the B software development process - from specification, through refinement and design, down to implementation and automatic code generation. The method uses a single uniform notation throughout development, designed to enable verification at each stage whilst placing particular emphasis on correctness.· Suitable for undergraduate and postgraduate courses on formal methods and software development· Written in a clear tutorial style of explanation · Contains numerous illustrative examples, exercises and self-testing questions with solutions throughout· Relevant to users of any B-Method CASE tool· Teaching materials available onlineThe B-Method : An Introduction also offers readers powerful tool support by providing a free licence for the B-Toolkit - an integrated toolset which supports and extends the entire B development lifecycle. Zusammenfassung This book provides a textbook introduction to the B-Method, a rigorous methodology for the development of correct software. The text covers all stages of the B software development process - from specification, through refinement and design, down to implementation and automatic code generation. The method uses a single uniform notation throughout development, designed to enable verification at each stage whilst placing particular emphasis on correctness. · Suitable for undergraduate and postgraduate courses on formal methods and software development · Written in a clear tutorial style of explanation · Contains numerous illustrative examples, exercises and self-testing questions with solutions throughout · Relevant to users of any B-Method CASE tool · Teaching materials available online The B-Method : An Introduction also offers readers powerful tool support by providing a free licence for the B-Toolkit - an integrated toolset which supports and extends the entire B development lifecycle. Inhaltsverzeichnis Preface.- Introducing Abstract Machines.- Review of Set Theory and Logic.- Weakest Preconditions.- Towards Machine Consistency.- Parameters, Sets and Constants.- Relations.- Functions and Sequences.- Arrays.- Nondeterminism.- Structuring with INCLUDES.- Structuring with SEES and USES.- Data Refinement.- Refinement of Nondetermnism.- Proof Obligations for Refinements.- Loops.- Implementation Machines.- Case Study: Heapsort.- Library Machines.- Answers to SelfTests.- Appendix A: Generalised Substitution Language.- Appendix B: Machine Readable AMN .- Index.- Index of Machines....
