COMP2111 Assignment 3
Ken Robinson 16th April 2012
Name of assignment: ass3
Due date: 27th April 2012 Assessment: 15 marks
Submission: give cs2111 ass3 Library.zip
1 Overview of assignment
This assignment extends the tutorial example of a simple library (see 2.4.2). The extensions are: 1. addition of a borrowing limit;
2. addition of a reservation capability
The assignment archive Library.zip contains the following components: Library ctx: context for Library machine;
List ctx: list context for LibraryR2
Each extension should be modelled as a refinement.
Note To create a refinement of a machine it is best to use the Event-B Explorer in Rodin; don’t create the refinement from scratch by hand.
In the Event-B Explorer right click on the machine you want to refine and then choose Refine from the options. Fill in the name of the refinement machine and Rodin will create a base for your refinement with all events being extended. In some cases you will not want an extension, for example when you want to modify the guards of an event, not simply add more guards. In such cases you will want to turn off extension for such events.
2 Refinements
2.1 LibraryR0: Borrowing limit
LibraryR0 is a very simple refinement that use the constant maxloan to set a borrowing limit on number of books that a member can borrow at any time. The constant does not have a value; it is simply of type N1. For animation with AnimB a value would be required in the AnimB values for Library ctx.
You should be try to discharge the proof obligations, but some are a little tricky. They probably will not be all auto-proved. You will have to use proof by cases (the dc button in the proof control) as most of the lemmas will have m ∈ members and there will be two cases: m = member and m ̸= member.
2.2 Adding book reservation
Book reservation is concerned with reserving a book that is currently borrowed. The following constraints apply to reservation of book by member:
Person reserving must be a member same as constraint for borrowing;
Book being reserved must be currently onloan
Book must not be currently reserved for member a book may be reserved at most once for any particular member;
Books may have multiple reservations by different members.
Reservations can be cancelled by the member that requested the reservation.
Modelling of reservation should be done in two stages represented by LibraryR1 and LibraryR2. LibraryR1 refines Library, and
LibraryR2 refines LibraryR1
2.3 LibraryR1
LibraryR1 should refine LibraryR0 and model reservation with no priority. That is, when a book that has been reserved is returned it can be borrowed by any one of the members who reserved that book.
A book cannot be reserved by the current borrower of the book.
2.4 LibraryR2
LibraryR2 should refine LibraryR1 and reservations should now satisfy the following:
1. Reservations are queued. That is reservations for the same book are queued in the order in
which the reservation requests were made.
2. When a reserved book is returned it is then available for the first member on the queue to borrow. The book is not available for general borrowing until all on the reservation queue have borrowed it.
3. A member who has requested reservation of a book can cancel their reservation, in which case the queue must “close up”.
This refinement will be a data refinement. 2.4.1 The List context
List ctx contains a list algebra that you should use for the book reservation queue. Lists are modelled as functions, so l(i) is the i-th element of the list l. There are two types of list models provided: LIST ordinary lists and ILIST injective lists, which are lists in which there are no repeated values. The algebra provides you with the following operations on lists:
APPEND APPEND(l 7→ m) appends m to the end of the list l, so you could write l := APPEND(l 7→ m);
程序代写 CS代考 加QQ: 749389476
DEQUEUE DEQUEUE(l) removes the head (first) item on the list, for example l := DEQUEUE(l);
JOIN JOIN(l1 7→ l2) joins the two lists l1 and l2, for example l := JOIN(l1 7→ l2);
DELETE DELETE(l 7→ i) deletes the i-th element of the list l, for example l := DELET E(l 7→ i).
IDELETE a slightly simpler version of DELETE that can be used on injective lists. IDELETE deletes the member m from the injective list l
l := IDELET E(l 7→ m).
The context provides quantifiers for determining dom, ran and indexing of list combinations. 2.4.2 What you should do
First, download the archive, Library.zip, containing the contexts Library ctx, List ctx and the machine Library.
Partial versions of the refinements are not included as it is best if you use Rodin to generate the initial refinements
Create and complete LibraryR0 to introduce a borrowing limit.
Create and modify LibraryR1 to add simple reservation and cancelling of a reservation.
Create and modify LibraryR2 to add a priority queue for reservation
Discharge or at least review the proof obligations it can be expected that the POs will be generally difficult, but they should be reviewed to detect errors in your models.
CONTEXT Library ctx SETS
MEMBER BOOK
axm1 : finite(MEMBER) axm2 : finite(BOOK) axm3 : maxloan ∈ N1
Code Help, Add WeChat: cstutorcs
MACHINE Library SEES Library ctx VARIABLES
books contained in the library members of the library
books borrowed by each member
INVARIANTS
inv1 : books ⊆ BOOK
inv2 : members ⊆ MEMBER
inv3 : borrowed ∈ books →7 members
EVENTS Initialisation
act1 : books := ∅ act2 : members := ∅ act3 : borrowed := ∅
Event NewMember =b
Add a new member of the library
grd1 : member ∈ MEMBER \ members then
act1 : members := members ∪ {member} end
Event AddBook =b
Add a book to the library; this could be a new book for the library or an extra copy
grd1 : book ∈ BOOK \ books then
act1 : books := books ∪ {book} end
Event Borrrow =b
A member borrows a book
grd1 : book ∈ books
grd2 : member ∈ members grd3 : book ∈/ dom(borrowed)
act1 : borrowed(book) := member end
Event Return =b
A member returns a book
grd1 : book ∈ dom(borrowed) then
act1 : borrowed := {book } ▹− borrowed end
CONTEXT List ctx
This context presents a small theory of lists.
Lists might also be called sequences.
Both injective and non-injective lists will be modelled. All elements of an injective list are distinct.
EXTENDS Library ctx CONSTANTS
Finite limit on length of lists Set of lists
Set of injective lists
List concatenation operator
Append an item to tail of list Append maintaining injectivity Delete head of list
Delete an element from any position of a list Delete an element from an injective list
axm1 : LENGTH ∈ N
axm2 : LIST = {l|l ∈ N1 →7 MEMBER ∧ dom(l) = 1 .. card(l)}
axm60 : finite(LIST)
axm3 : ∅ ∈ LIST
axm4:ILIST={l|l∈LIST∧l∈N17 MEMBER}
axm5 : ILIST ⊂ LIST
axm6 : ∅ ∈ ILIST
axm7: ∀l·l ∈ILIST ⇔l ∈LIST ∧l ∈1 ..LENGTH 7 MEMBER
axm8: ∀l·l∈LIST⇒ran(l)=l[dom(l)]
axm9: ∀l·l∈LIST⇒ran(l)=l[1..card(l)]
axm10: ∀l·l ∈LIST ∧card(ran(l))=card(dom(l)) ⇒ l ∈ ILIST
axm11 : JOIN ∈ (LIST × LIST ) → LIST
axm12 : dom (JOIN ) = LIST × LIST
axm13: ∀l1,l2·l1∈LIST∧l2∈LIST ⇒
dom(JOIN(l1 7→l2))=1 ..card(l1)+card(l2)
axm14: ∀l1,l2,i·l1 ∈LIST ∧l2 ∈LIST ∧i ∈dom(JOIN(l1 7→l2)) ⇒
(i ∈1 ..card(l1)⇒JOIN(l1 7→l2)(i)=l1(i)) ∧
(i − card(l1) ∈ 1 .. card(l2) ⇒ JOIN(l1 7→ l2)(i) = l2(i − card(l1))) 7
axm15 : ∀l·l ∈ LIST ⇒
JOIN (l 7→ ∅) = l
axm16 : ∀l·l ∈ LIST ⇒
JOIN(∅ 7→ l) = l
axm17: ∀l1,l2·l1 ∈ILIST ∧l2 ∈ILIST ∧ran(l1)∩ran(l2)=∅ ⇒
JOIN (l1 7→ l2 ) ∈ ILIST
axm18: ∀l1,l2·l1∈LIST∧l2∈LIST ⇒
ran(JOIN(l1 7→ l2)) = ran(l1) ∪ ran(l2)
axm19: ∀l1,l2·l1∈LIST∧l2∈LIST ⇒
card(JOIN(l1 7→l2))=card(l1)+card(l2) axm20 : APPEND ∈ (LIST × MEMBER) → LIST
axm21 : dom(APPEND) = LIST × MEMBER
axm22: ∀l,m·l∈LIST ⇒
dom(APPEND(l 7→ m)) = 1 .. card(l) + 1
axm23: ∀l,m,i·l ∈LIST ∧i ∈dom(APPEND(l 7→m)) ⇒
(i ∈ dom(l) ⇒ APPEND(l 7→ m)(i) = l(i)) ∧
(i = card(l) + 1 ⇒ APPEND(l 7→ m)(i) = m)
axm24: ∀l,m·l∈LIST∧m∈MEMBER ⇒
ran(APPEND(l 7→ m)) = ran(l) ∪ {m}
axm25: ∀l,m·l∈LIST∧m∈MEMBER ⇒
card(APPEND(l 7→ m)) = card(l) + 1
axm26: ∀l,m·l∈ILIST∧m∈MEMBER∧m∈/ran(l) ⇒
APPEND(l 7→ m) ∈ ILIST
axm27 : IAPPEND ∈ (ILIST × MEMBER) → ILIST
axm28 : dom(IAPPEND) = ILIST × MEMBER
axm29: ∀l,m·l∈LIST ⇒
dom(IAPPEND(l 7→ m)) = dom(APPEND(l 7→ m))
axm30: ∀l,m·l∈ILIST∧m∈/ran(l) ⇒
IAPPEND(l 7→ m) = APPEND(l 7→ m)
axm31: ∀l,m·l∈LIST∧m∈MEMBER ⇒
card(APPEND(l 7→ m)) = card(l) + 1 8
axm32 : DEQUEUE ∈ LIST → LIST
axm33 : dom(DEQUEUE) = LIST
axm34: ∀l·l∈LIST∧l̸=∅ ⇒
dom(DEQUEUE(l)) = 1 .. card(l) − 1
axm35: ∀l,i·l∈LIST∧l̸=∅∧i∈1..card(l)−1 ⇒
DEQUEUE(l)(i) = l(i + 1)
axm36: ∀l·l∈ILIST∧l̸=∅ ⇒
DEQUEUE(l) ∈ ILIST
axm37: ∀l·l∈LIST∧l̸=∅ ⇒
ran(DEQUEUE(l)) = ran(l) \ {l(1)} axm38 : DELETE ∈ (LIST × (1 .. LENGTH )) →7 LIST
axm39: dom(DELETE)⊆LIST ×(1 ..LENGTH)
axm40: ∀l,i·l∈LIST∧i∈dom(l) ⇒
l 7→ i ∈ dom(DELETE)
axm41: ∀l,i·l∈LIST∧i∈dom(l) ⇒
dom(DELETE(l 7→ i)) = 1 .. card(l) − 1
axm42: ∀l,i,j·l ∈LIST ∧i ∈dom(l)∧j ∈1 ..card(l)−1 ⇒
j ∈ dom(DELETE(l 7→ i))
axm43: ∀l,i,j·l∈LIST∧i∈dom(l)∧j∈1..i−1 ⇒
DELETE(l 7→ i)(j) = l(j)
axm44: ∀l,i,j·l∈LIST∧i∈dom(l)∧j∈i..card(l)−1 ⇒
DELETE(l 7→ i)(j) = l(j + 1)
axm45: ∀l,i·l∈LIST∧i∈dom(l) ⇒
card(DELETE(l 7→ i)) = card(l) − 1
axm46: ∀l,i·l∈LIST∧i∈dom(l) ⇒
ran(DELETE(l 7→ i)) = ran(l) \ {l(i)}
axm47: ∀l,i·l∈LIST∧i∈dom(l) ⇒
card(DELETE(l 7→ i)) = card(l) − 1 axm48 : IDELETE ∈ (ILIST × MEMBER) →7 ILIST
axm49 : dom(IDELETE) = ILIST × MEMBER
axm50: ∀l,m·l∈ILIST∧m∈MEMBER∧m∈ran(l) ⇒
l 7→ m ∈ dom(IDELETE)
axm51: ∀l,m·l∈ILIST∧m∈ran(l) ⇒
dom(IDELETE(l 7→ m)) = 1 .. card(l) − 1
axm52: ∀l,m·l∈ILIST∧m∈ran(l) ⇒
IDELETE(l 7→ m) = DELETE(l 7→ l−1 (m))
axm53: ∀l,m·l∈ILIST∧m∈ran(l) ⇒
card(IDELETE(l 7→ m)) = card(l) − 1
axm54: ∀l,m·l∈ILIST∧m∈ran(l) ⇒
ran(IDELETE(l 7→ m)) = ran(l) \ {m}
axm55: ∀l·l∈LIST∧l̸=∅ ⇒
DEQUEUE(l) = DELETE(l 7→ 1)
axm56: ∀l·l∈LIST∧l̸=∅ ⇒
card(DEQUEUE(l)) = card(l) − 1
axm57: ∀l,i·l∈ILIST∧i∈dom(l) ⇒
DEQUEUE(l) ∈ ILIST
axm58: ∀l,i·l∈ILIST∧i∈dom(l) ⇒
DELETE(l 7→ i) ∈ ILIST
axm59: ∀l,m·l∈LIST∧m∈MEMBER ⇒
DELETE(APPEND(l 7→ m) 7→ card(l) + 1) = l
Programming Help