Software Engineering: Formal Specification of Library System Project

This document presents a formal specification of a library system, designed to manage books and borrowers effectively. It utilizes the Z schema to define the system's state and operations. The system includes functionalities to add, delete, and lend books, as well as add and delete borrowers. The schema incorporates pre-conditions and post-conditions for each operation, ensuring data integrity. For example, the AddBook operation differentiates between lending and reference books, preventing duplicates and ensuring accurate record-keeping. The DeleteBook operation considers whether a book is on loan, and the DeleteBorrower operation checks if a borrower has any books on loan. The LendBook operation enforces conditions such as borrower status, book availability, and borrowing limits. The system also addresses late returns and calculates fines. Overall, this specification provides a robust framework for managing a library's resources and interactions.

Library System (LS)
Just like any other library that uses information technology to manage the lending and return of
the books, this library records and provide information about the books available and the
borrowers. (Belafi, et al., 2019) The Z schema starts by declaring two sets (Book, Person), thus
identifying the major parts of the library system using the schema below.
Library
onLoan, onShelves, books, lendingBook, referenceBook: ℙ Book
borrowers: ℙ Person
lentTo: Book ⇸ Person
onLoan = dom lentTo
ran lentTo ⊆ borrowers
onLoan ∪ onShelves = books
onLoan ∩ onShelves = ∅
For example, let initial values be as following;
On loan = 5
On shelves =5
Lending books = 10
Reference books = 10
Books = 20
Borrowers = 5
Library

onLoan, onShelves, books, lendingBook, referenceBook: ℙ Book
borrowers: ℙ Person
lentTo: Book ⇸ Person
onLoan = dom lentTo
ran lentTo ⊆ 5
10 ∪ 10 = 20
5 ∩ 5 = ∅
It is important to note that in the system, books are categorized as lending or referenceBook
where the two categories can be found either onShelves or onLoan. The relationship that exists
between a person and a book in this library system is lentTo. For purposes of effective
management of the library, it is also important to limit the number of books that a borrower can
be allowed to borrow and in this case, a borrower is allowed to borrow a maximum of 5 books.
In order to make the system effective, this condition must be met. (Vijayasarathy & Butler, 2015)
limit: ℕ
limit ∈ 1.. 5
As stated in the introductory part, this Library Management Systems (LMS) was designed to
perform the following task.
(a) 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. The system will give
feedback ‘Book is in the library' if the book already exists in the system and no changes will
be effected in the information stored. The feedback response of the system after successfully
adding the book will be ‘Book added'. In order to differentiat between reference books and

lending categories, the z schema was entered the AddBook(lendingBook) and the
AddBook(referenceBook). In order to eliminate the errors of adding a book that already
exists in the library, the Book_in_the_library was entered in the schema. This also ensures
that no changes are effected in the information stored in the system. The z schema for add a
book for both categories (lendingBook and referenceBooks) appears as follows.
AddBook(lendingBook)
Δ Library
b? : Book
r! : SystemResponse
b? ∉ Books
onLoan′ = onLoan
onShelves′ = onShelves ∪ {b?}
books′ = Books ∪ {b?}
lendingBook′ = LendingBook ∪ {b?}
referenceBook′ = ReferenceBook
borrowers′ = Borrowers
lentTo′ = lentTo
r! = BookAdded
AddBook(referenceBook)
Δ Library
b? : Book
r! : SystemResponse
b? ∉ books
onLoan′ = onLoan
onShelves′ = onShelves ∪ {b?}
books′ = books ∪ {b?}

lendingBook′ = LendingBook
referenceBook′ = ReferenceBook ∪ {b?}
borrorws′ = Borrowers
lentTo′ = lentTo
r! = BookAdded
It is important to understand that b? ∉ Book is used as a pre-condition that must hold and it
allows the AddBook to take place. This is followed by post-conditions which are the changes
that should take place in the system. The z schema for the response ‘Book already in the library’
is as follows:
Book_in_the_library
Δ Library
b? : Books
r! : SystemResponse
b? ∈ Books
onLoan′ = onLoan
onShelves′ = onShelves
books′ = Books
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = Borrowers
lentTo′ = lentTo
r! = Book_in_the_library
Example
Book title = System Analysis And Design (SAAD)
Category = lending book
Price = $120

AddBook(lendingBook)
Δ Library
b? : SAAD
r! : SAAD added
b? ∉ books
onLoan′ = 5
onShelves′ = 5 ∪ {b?}
books′ = 20 ∪ {b?}
lendingBook′ = 10 ∪ {b?}
referenceBook′ = 10
borrowers′ = 5
lentTo′ = lentTo
r! = SAAD added
(b) Add a borrower: This task is performed if the borrower is new and his/her personal details
need to be stored in the system. When the task has been performed successfully, the system
response with ‘Borrower added'. However, if the borrowers' details already exist in the
system, the response of the system will be ‘Ticket allocated' and this means there are no
changes effected in the system. When adding a borrower, the operation can either be
successful or not. The AddBorrower and Ticket_allocated schemas describe these operations
respectively.

AddBorrower
Δ Library
r! : SystemResponse
p? : Person
p? ∉ Borrower
books′ = Books
onShelves′ = onShelves
onLoan′ = onLoan
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = Borrowers ∪ {p?}
lentTo′ = LentTo
r! = BorrowerAdded
Ticket_allocated
Δ Library
p? : Person
r! : SystemResponse
p? ∈ Borrower
books′ = Books
onLoan′ = onLoan
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = Borrowers
lentTo′ =lentTo
r! =Ticket_allocated
Example
Borrower = John

AddBorrower
Δ Library
p? : John
r! : John added
p? ∉ borrowers
books′ = 20
onShelves′ = 6
onLoan′ = 5
lendingBook′ = 11
referenceBook′ = 10
borrowers′ = 5 ∪ {p?}
lentTo′ = LentTo
r! = John added
c) Delete a book:
There are two conditions to be met for the changes to take place in the system: The book is not a
property of the library and the response from the system will be ‘Not a library book’. If the status
of the book shows that it is out on loan and the response from the system will be ‘Return book
first’. No changes will be effected in the system if the two conditions are not satisfied.
Otherwise, the operation will be successful and the output from the system is ‘Book deleted'
shall be output to screen. Two operations are used to differentiate the two type of books in the
library; the DeleteBook (lendingBook) and the DeleteBook (referenceBook). In order to ensure
that the two conditions stated above are satisfied, two operations are entered into the schema; the
Return_book_first and Not_in_library schemas. These operations also ensure that errors are
eliminated during a process of deleting the book.

DeleteBook(lendingBook)
Δ Library
b?: Book
r?: SytemResponse
b? ∈ books ∖ ran lentTo
onLoan′ = onLoan
onShelves′ = onShelves ∖ {b?}
books′ = Books ∖ {b?}
lendingBook′ = LendingBook ∖ {b?}
referenceBook′ = ReferenceBook
borrowers′ = Borrowers
lentTo′ = lentTo
r! = BookDeleted
DeleteBook(referenceBook)
Δ Library
b? : Book
r! : SystemResponse
b? ∈ books ∖ ran lentTo
onLoan′ = onLoan
onShelves′ = onShelves ∖ {b?}
books′ = Books ∖ {b?}
lendingBook’ = LendingBook
referenceBook′ = ReferenceBook ∖ {b?}
borrowers′ = Borrowers
lentTo′ = lentTo
r! = BookDeleted

Not_in_library
Δ Library
b? : Books
r! : SystemResponse
b? ∉ Books
onLoan′ = onLoan
onShelves′ = onShelves
books′ = Books
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = Borrowers
lentTo′ = lentTo
r! = Not_in_library
Return_book_first
Δ Library
b? : Books
r? : SystemResponse
b? ∈ dom lentTo
onLoan′ = onLoan
onShelves′ = onShelves
books′ = books
lendingBook′ = lendingBook
referenceBook′ = referenceBook
borrowers′ = borrowers
lentTo′ = lentTo
r! = Return_book_first
Example
Let’s delete the SAAD book.

DeleteBook(lendingBook)
Δ Library
b?: SAAD
r?: SAAD deleted
b? ∈ books ∖ ran lentTo
onLoan′ = 5
onShelves′ = 6 ∖ {b?}
books′ = 20 ∖ {b?}
lendingBook′ = 11 ∖ {b?}
referenceBook′ = 10
borrowers′ = 6
lentTo′ = lentTo
r! = SAAD deleted
The same happens when deleting a reference book.
d) Delete a borrower: Similarly, there are pre-conditions that should be satisfied for the changes
to occur in the system. The first pre-condition is that the borrower must be recorded in the
system and there is no data indicating that the borrower is recorded in the system, the
response is ‘Not a borrower’. The second pre-condition is that the borrower must not have a
book on loan. If he/she has a book on loan, the output is ‘Borrower has books on loan’ and
not changes occurs in the system. Upon successful deletion of a borrower from the system,
the response is ‘Borrower deleted’. Therefore, three operations are entered in the schema:
The DeleteBorrower; the Borrower_has_onLoan; and Not_a_borrower. The first operation
instructs the system to delete the details of a borrower who is not recorded to have a book on
loan. The second and third operations eliminate the errors of deleting a borrower who is not
in the system and who has a book on loan.

DeleteBorrower
Δ Library
r? : SystemResponse
p? : Person
p? ∈ Borrowers ∖ ran lentTo
books′ = Books
onLoan′ = onLoan
onShelves′ = onShelves
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = Borrowers ∖ {p?}
lentTo′ = lentTo
r! = BorrowerDeleted
Not_a_borrower
Δ Library
r! : SystemResponse
p? ∉ borrowers
books′ = Books
onLoan′ = onLoan
onShelves′ = onShelves
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = Borrowers
lentTo′ = lentTo
r! = Not_a_borrower

Borrower_has_books_onLoan
Δ Library
p? : Person
r! : SystemResponse
p? ∈ ran lentTo
onLoan′ = onLoan
onShelves = onShelves
books′ = Books
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = Borrowers′
lentTo′ = lentTo
r! = Borrower_has_books_onLoan
Example
Delete John
DeleteBorrower
Δ Library
p? : John
r? : John Deleted
p? ∈ borrowers ∖ ran lentTo
books′ = 20
onLoan′ = 5
onShelves′ = 5
lendingBook′ = 10
referenceBook′ = 10
borrowers′ = 5 ∖ {p?}
lentTo′ = lentTo
r! = John deleted
e) Lend a book: This task has three pre-conditions that should be fulfilled for the changes to
occur in the system. The first pre-condition is that the person must be a borrower and if
he/she is not a borrower, no changes occur in the system and the response is ‘Not a