Desklib - Online Library for Study Material and Solved Assignments

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