Group Formal Specification of a Library System - ITECH7410, Sem 1

This assignment focuses on the formal specification of a library system, designed to manage book lending, returns, and reservations. The solution begins with an overview of the system's functionalities, including adding and deleting books and borrowers, lending and returning books, and managing reservations. The Z schema is used to define the system's major components, specifically the Book and Person sets. Non-trivial predicate statements defining book, librarian, student, and reservation details are also provided. The assignment covers various system functionalities such as enquiring about books and reservations, and cancelling reservations. The solution addresses the core aspects of library management, providing a detailed understanding of how the system operates and manages its resources. This document, available on Desklib, offers a comprehensive solution for students studying software engineering methodologies.

Library Management system
 manage the lending and return of the books.
 Records and provide information about the books
available and the borrowers.
 The Z schema starts by declaring two sets (Book,
Person), thus identifying the major parts of the
library system

System functionalities
Add a book:
 This is the first task this library system is designed to do.
 The book will be added into the library only if it does not already
exist in the library.
Add a borrower:
 A borrower is added to the system if his/her details are not in the
system.
 If the details exist, the system respond the a ticket was allocated

System functionalities
Delete a book:
 The book must be a property of the library.
 The book has to be on shelves and not on loan.
 The system checks if the two conditions are met and then gives a
response.
Delete a borrower:
 The borrower must be in the system
 The borrower must not have a book.
 If the two conditions are met, the system deletes the borrower and
give a response.

System functionalities
Lend a book:
 There are two conditions:
 The book must be on shelves and the borrower must be registered.
 The system checks this condition and then lend that book.
Return a book:
 The book must be a property of the library
 The book must be out on loan.
 The response is ‘Not a library book' and ‘Not on loan' respectively and no
changes occurs in the system.
 Then the system adds the book to on shelves.

System functionalities
Enquire about a book:
 This function is used to check whether the book is on loan or on shelves.
 The system gives a response as to whether the book is on loan or on shelves
Reserve a book:
 The book is only reserved by a borrower.
 Only books belonging to the library are reserved.
 Definition of the title, reserved and heldFor are new features that has to
added to the system.
 Every book has a title and a title is reserved by a person for whom the
book is held.

System functionalities
Enquire about a reservation:
 This task involves checking whether the title of the book the
borrower is interested in borrowing is reserved.
 ReserveBook function ensures that the person is a borrower.
Cancel a reservation:
 This is a situation where the borrower does not want to reserve
the book anymore.
 In essence, this is a reverse of reservation and the function used is
Cancel_reservation.

Non-trivial predicate statements
 These are statements that are predictable and they can
either be true or false.
 Book Details BookID, BookName, BookPrice, pages⇒
 Librarian Details → Name, ID, PhoneNumber, Email
 Student Details ID, Student name, PhoneNumber,∃ ⇔
Email
 Reservation Details Type, Reference number,∃ ⇔
payment details, student ID