Formal Specification:

Introduction

Each of the following questions requires the construction of an Event-B model. For each model, you should provide appropriate invariants and prove that your model satisfies these invariants.

Question 1 :

A primary school class contains a number of children and a variety of books. Write a model which keeps track of the books that the children have read. It should maintain a relation hasread between children and books. It should also handle the following events:

record: adds the fact that the given child has read the given book

newbook: outputs a book that the given child has not already read

books_query: outputs the number of books the given child has read