Jean-Raymond Abrial, Z, Socrate, B, Event-B, Rodin

 Foreword of the book "SPECIFICATION CASE STUDIEs" edited by Ian Hayes Reading formal texts is like meeting people. Sometimes, you understand them straightaway like good friends who take to each other immediately. At other times, it is more difficult. You may parse what you read, but find it impossible to work out any meaning. With the latter, you have to be patient, ask questions, explore the surroundings; in other words, it is better for you to be introduced through some common good friends who volunteer to help you prepare for the first meeting. Large computer programs, to say the least, pertain to the category of formal texts whose meanings are not immediately obvious! For that reason, people have been trying – for some time – to find out what kind of intermediate text would be best suited to play the role of go-between. This book reports on experiments made at Oxford University within this frame- work: it shows how one may communicate ideas and meanings about existing (o...

    https://staff.itee.uq.edu.au/ianh/Papers/SCS2.pdf SPECIFICATION CASE STUDIES Second Edition Copyright c© 1987, 1992 Prentice Hall International (UK) Ltd Appendices A and B may be copied for educational purposes. Edited by Ian Hayes With Contributions by Bill Flinn Roger Gimson Steve King Carroll Morgan Ib Holm Sørensen Bernard Sufrin ii Contents I Tutorials 1 1 Small examples of specification using mathematics 3 Ian Hayes 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 A symbol table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 File update . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.4 Sorting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.5 Solutions to exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2 Block-structured symbol table 13 Ian Hayes 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Sy...