UQ Students should read the Disclaimer & Warning

Note: This page dates from 2005, and is kept for historical purposes.

COMP3601 – Software Specification – Assignment One (Library Machine)

Specification (PDF, 105 KB)

I achieved 19 out of a possible 20 marks.

My Solution (PDF, 30 KB)

Source used to generate the pretty-printed solution above, is shown below.

ALibrary.mch
/*" {\bf COMP3601 - Assignment 1} {\bf Name: Ned Martin} {\bf Student Number: 40529927} "*/ MACHINE Library SETS BOOKID; BOOKDESC; READERID; READERDESC; LOANTYPE CONSTANTS maxloans PROPERTIES maxloans : NAT VARIABLES books, readers, reserved, onLoanTo, today, loanTypeDuration, bookLoanType, returnDayOfBook INVARIANT books : BOOKID +-> BOOKDESC & readers : READERID +-> READERDESC & reserved : POW BOOKID & onLoanTo : BOOKID +-> READERID & today : NAT & loanTypeDuration : LOANTYPE --> NAT & bookLoanType : BOOKID +-> LOANTYPE & returnDayOfBook : BOOKID +-> NAT & reserved <: (dom(books) - dom(onLoanTo)) & dom(onLoanTo) <: dom(books) & ran(onLoanTo) <: dom(readers) & ! rr . (rr : dom(readers) => ( card(onLoanTo |> {rr}) <= maxloans) ) & /* Only library books have a loan type */ dom(bookLoanType) <: dom(books) & /* All borrowed books have a loan type */ dom(onLoanTo) <: dom(bookLoanType) & /* No reserved book has a loan type */ reserved /\ dom(bookLoanType) = {} & /* A book is on loan if and only if it has a return date */ dom(onLoanTo) = dom(returnDayOfBook) INITIALISATION books, readers, reserved, onLoanTo, today, loanTypeDuration, bookLoanType, returnDayOfBook := ( {},{},{},{},0,{xx, yy | xx : LOANTYPE & yy : NAT},{},{} ) OPERATIONS borrow_book(bookNo, readerNo) = PRE bookNo : dom(books) - ( (reserved \/ dom(onLoanTo)) ) & readerNo : dom(readers) & card(onLoanTo |> {readerNo}) < maxloans & /* Book has a loantype */ bookNo : dom(bookLoanType) THEN onLoanTo := onLoanTo <+ { bookNo |-> readerNo} || /* Return date of book = bookNo |-> (N + today) where N = N from BOOKID |-> LOANTYPE |-> N */ returnDayOfBook := returnDayOfBook <+ {bookNo |-> ((bookLoanType ; loanTypeDuration)(bookNo) + today)} END; remove_book(bookNo) = PRE bookNo : BOOKID & bookNo : dom(books) & bookNo /: dom(onLoanTo) THEN books := {bookNo} <<| books || reserved := reserved - {bookNo} || /* Remove book with bookNo from bookLoanType */ bookLoanType := {bookNo} <<| bookLoanType END; add_to_reserve(bookNo) = PRE bookNo : dom(books) - dom(onLoanTo) & bookNo /: reserved THEN reserved := reserved \/ {bookNo} || bookLoanType := {bookNo} <<| bookLoanType END; new_day = PRE true THEN /* Increment today */ today := today + 1 END; change_loan_type(bookNo, newLoanType) = PRE bookNo : dom(books) & bookNo /: reserved & newLoanType : LOANTYPE THEN /* Insert/modify {bookNo |-> newLoanType} in bookLoanType */ bookLoanType := bookLoanType <+ {bookNo |-> newLoanType} END; change_duration(loanType, newDuration) = PRE loanType : LOANTYPE & newDuration : NAT THEN /* Insert/modify {loanType |-> newDuration} into loanTypeDuration */ loanTypeDuration := loanTypeDuration <+ {loanType |-> newDuration} END; ob <-- overdue_books = PRE true THEN /* Return ob where ob = {BOOKID |-> READERID} if returnDay(bookID) < today and was onloan */ ob := {xx | xx : dom(returnDayOfBook) & returnDayOfBook(xx) < today} <| onLoanTo END END
Portions of code © Copyright 2004 Ned Martin

04-Jun-2004