Desklib - Online Library for Study Material and Solved Assignments

Desklib is an online library that offers a wide range of study material, including solved assignments, essays, and dissertations. It provides access to relevant content for various courses and subjects. Whether you need help with your assignments or want to enhance your knowledge, Desklib has you covered.

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

borrower'. The second pre-condition is that the book should be a library property for the
changes to occur and if the book is not a library property, the response from the system is
‘Not a library book'. The third pre-condition is that the book should be in shelves and not out
on loan and if the book is out on loan the response is ‘Return book first' and not changes
occurs in the system. If all the pre-conditions have been satisfied, the changes in the system
occur and the book is lent to a borrower. The response from the system after successful
execution of the operations is ‘Book lent to borrower'. It is important to note that only
lending books are borrowed from the library and reference book should not be borrowed
from the library. Therefore, if the book is categorized as a referenceBook, the response from
the system is ‘Reference book not to be borrowed’
The following functions are entered in the schema in order to successfully execute the tasks
as intended:
the Lend_book_ok(lendingBook) which is designed to ensure that the borrower is in the
system and the book available, as well as the borrower, does not exceed the book limit.
The dateBorrowed is a new function that addresses the issues of late returns, and calculates
the fine for the exceeded time and adds into the borrowers' record.

Lend_book_ok(lendingBook)
Δ Library
b? : Book
d? : Date
p? : Person
r! : SystemResponse
p? ∈ Borrower
b? ∈ stock ∖ dom lentTo
♯ dom (lentTo ▷ {p?} <= limit
stock′ = stock ∖ dom lentTo
borrowers′ = Borrowers
onShelves′ = onShelves
onLoan′ = onLoan ∪ dom lentTo
books′ = Books
lentTo’ lentTo ⊕ {b? ↦ p?}
dateBorrowed′ = dateBorrowed ⊕ {b? ↦p?}
owes′ = Owes
r! = Book_lentTo_borrower
For example lending a book that is already in the library to a borrower say Peter who is already a
borrower on May 22, 2019

Lend_book_ok(lendingBook)
Δ Library
b? : SAAD
d? : May 22, 2019
p? : Peter
r! : Book rented to Peter
p? ∈ borrowers
b? ∈ stock ∖ dom lentTo
♯ dom (lentTo ▷ {p?} <= limit
stock′ = 20 ∖ dom lentTo
borrowers′ = 5
onShelves′ = 4
onLoan′ = 6 ∪ dom lentTo
books′ = 20
lentTo’ lentTo ⊕ {b? ↦ p?}
dateBorrowed′ = May 22, 2019 ⊕ {b? ↦p?}
owes′ = 1
r! = book rented to Peter
Since all the other errors that are likely to occur when lending a book are already covered, the
following function addresses the issue of books categorized as a reference and cannot be
borrowed from the library: The Reference_book.

Reference_book
Δ Library
b? : Book
r! : SystemResponse
b? ∈ referenceBook
onLoan′ = onLoan
onShelves′ = onShelves
books′ = Books
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = borrowers
lentTo′ = lentTo
r! = ReferenceBook_book_not_to_be_borrowed
For example when trying to lend a reference book
Reference_book
Δ Library
b? : APA Style Guide
r! : APA Style Guide not to be borrowed
b? ∈ referenceBook
onLoan′ = 5
onShelves′ = 5
books′ = 20
lendingBook′ = 10
referenceBook′ = 10
borrowers′ = 5
lentTo′ = lentTo
r! = APA Style Guide not to be borrowed
f) Return a book: Two pre-condition must be satisfied for the changes to occur in the system.
The first pre-condition is that the book must be a property of the library and the second pre-
condition is that 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. Upon meeting the two pre-

condition, the system accepts the return of the book to the shelves and the records of being
lent out to a borrower changes and the response is ‘Book returned'. In order to successfully
complete the operations, the Return_book function must be executed in the schema. (Taieb, et
al., 2017)
Return_book
Δ Library
b? : Book
r! : SystemResponse
b? ∈ dom lentTo
onLoan′ = onLoan ∖ {b?}
onShelves′ = onShelves ∪ {b?}
books′ = Books
lending′ = Lending ∪ {b?}
referenceBook′ = ReferenceBook
borrowers′ = Borrowers ∖ {p?}
lentTo′ = {b?} ⩤ lentTo
r! = BookReturn
Example

Return_book
Δ Library
b? : SAAD
r! : SAAD returned
b? ∈ dom lentTo
onLoan′ = 5 ∖ {b?}
onShelves′ = 5 ∪ {b?}
books′ = 20
lending′ = 10 ∪ {b?}
referenceBook′ = 10
borrowers′ = 5 ∖ {p?}
lentTo′ = {b?} ⩤ lentTo
r! = SAAD returned
Not_onLoan
Δ Library
b? : Book
r! : SystemResponse
b? ∉ dom lenTo
onLoan′ = onLoan
onShelves′ = onShelves
books′ = Books
lending′ = Lending
referenceBook′ = ReferenceBook
borrowers = Borrowers
lentTo′ = lentTo
r! = Not_onLoan
Where the book is returned late, the function RateReturn is used to calculate the fine and add into
the borrower records as shown below.

RateReturn
Δ Library
today? : Date
dateBorrowed′ = {b?} ⩤ dateBorrowed ∧ (Diff ((dateBorrowed b?) today?) <
period ∧ owes′ = owes) ∨ (Diff ((dateBorrowed b?) today?) > period ∧
owes′ = owes ⊕ {lentTo b? ↦ (owes lentTo b? + (Diff ((dateBorrowed b?) | today?) –
period) * fine}))
g) Enquire about a book: This library system also performs the task of enquiring whether the
book is out on loan or available in the shelves. This involves the use of the function
Enquire_book.
Enquire_book
Δ Library′
t? : Title
r! : SystemResponse
t? ∈ title ∖ ran lentTo
onLoan′ = onLoan ∖ {t?}
onShelves′ = onShelves ∪ {t?}
books′ = Books
lendingBook′ = LendingBook ∪ {t?}
referenceBook′ = ReferenceBook
r! = Book_onShelves
Example

Enquire_book
Δ Library′
t? : SAAD
r! : SAAD on shelve
t? ∈ title ∖ ran lentTo
onLoan′ = 5 ∖ {t?}
onShelves′ = 5 ∪ {t?}
books′ = 20
lendingBook′ = 10 ∪ {t?}
referenceBook′ = 10
r! = SAAD on shelve
h) Reserve a book: There are two pre-conditions made for the changes to occur in the system.
The first pre-condition is that the book is only reserved by a borrower. The second pre-
condition is that only books belong to the library are reserved. In order to allow the library
system to perform this task, extra new features have to be added to the initial library system.
These are the definition of the title, reserved and heldFor by the new function. Every book
has a title and a title is reserved by a person for whom the book is held.
Library′
Library′
title: Book ⇸ Title
heldFor: Book ⇸ Person
reserved: Title ⇸ Person
dom title = stock
dom reserved = ran title
∀t: Title | t ∈ dom reserved * ran (reserved t) ⊆ borrower
dom heldFor ⊆ stock ∖ dom lentTo
ran heldFor ⊆ borrower

ReserveBook
Δ Library′
t? : Title
p? : Person
p? ∈ borrower
t? ∈ ran title
reserves′ = reserved ⊕ {t? ⇸ reserve t? ^ <p?>}
title′ = title
heldFor′ = heldFor
Example
Reserving SAAD for John and there are 5 books already reserved
ReserveBook
Δ Library′
t? : SAAD
p? : John
p? ∈ borrower
t? ∈ ran title
reserves′ = 5 ⊕ {t? ⇸ reserve t? ^ <p?>}
title′ = SAAD
heldFor′ = heldFor
i) Enquire about a reservation: This task involves checking whether the title of the book the
borrower is interested in borrowing is reserved and ReserveBook function ensures that the
person is a borrower.

Enquire
Δ Library′
t? : Title
title′ = title ∪ {b? ⇸ t?}
t? ∉ dom reserved ∧ reserved′ = reserved ∪ {t? ↦ reserved t? ^ <p?>}
title′ = title
heldFor′ = heldFor
Example
Enquire
Δ Library′
t? : SAAD
title′ = SAAD ∪ {b? ⇸ t?}
t? ∉ dom reserved ∧ reserved′ = 5 ∪ {t? ↦ reserved t? ^ <p?>}
title′ = SAAD
heldFor′ = Held by John
j) 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 is the
Cancel_reservation.
Cancel_reservation
Δ Library′
t? : Title
p? : Person
t? ∉ ran title
p? ∉ borrowers
cancelReserved′ = cancelReserved ⊕ {t? ↦ cancelReserved t? ^ <p?>}
title′ = title
cancel_heldFor′ = cancel_heldFor

Example
Cancel_reservation
Δ Library′
t? : SAAD
p? : John
t? ∉ ran title
p? ∉ borrowers
cancelReserved′ = cancelReserved ⊕ {t? ↦ cancelReserved t? ^ <p?>}
title′ = SAAD
cancel_heldFor′ = john canceld reservation
k) Buy a book: This task has two pre-conditions that should be fulfilled for the changes to occur
in the system. The first pre-condition is that the book should be a library property for the
changes to occur and if the book is not a library property, the response from the system is
‘Not a library book'. The second pre-condition is that the book should be in shelves and not
out on loan and if the book is out on loan the response is ‘Return book first' and not changes
occurs in the system. If all the pre-conditions have been satisfied, the changes in the system
occur and the book is lent to a borrower. The response from the system after successful
execution of the operations is ‘Book bought by a borrower'. It is important to note that only
lending books are sold from the library and reference book should not to be sold from the
library. Therefore, if the book is categorized as a referenceBook, the response from the
system is ‘Reference book not to be sold’
The following functions are entered in the schema in order to successfully execute the tasks
as intended:
the Sold_book_ok(lendingBook) which is designed to ensure that the book sold is not
already out on loan.

Sold_book_ok(lendingBook)
Δ Library
b? : Book
p? : Person
r! : SystemResponse
p? ∈ Borrowers
b? ∈ stock ∖ dom sellTo
♯ dom (sellTo ▷ {p?} <= limit
stock′ = stock ∖ dom sellTo
onLoan′ = onLoan ∪ dom lentTo
onShelves′ = onShelves
books′ = Books
borrowers′ = Borrowers
sellTo’ sellTo ⊕ {b? ↦ p?}
dateBorrowed′ = dateBorrowed ⊕ {b? ↦p?}
owes′ = Owes
r! = Book_bought_by_a_borrower
After the book is successfully sold, that book needs to be deleted from the library. The function
DeleteBook(lendingBook) is used to ensure this.

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
The following function addresses the issue of books categorized as a reference and cannot be
bought from the library: The Reference_book.
Reference_book
Δ Library
b? : Book
r! : SystemResponse
b? ∈ referenceBook
onLoan′ = onLoan
onShelves′ = onShelves
books′ = Books
lendingBook′ = LendingBook
referenceBook′ = ReferenceBook
borrowers′ = borrowers
sellTo′ = sellTo
r! = ReferenceBook_book_not_to_be_sold
l) Receive a book: The library also gives a notice when the book sold is received by the buyer.
The function book_received_ok is used to make this notice. A message ‘book received' is
displayed.

book_received_ok
Δ Library
b? : Book
r! : SystemResponse
b? ∈ dom sellTo
onLoan′ = onLoan ∖ {b?}
onShelves′ = onShelves ∪ {b?}
books′ = Books
lending′ = Lending ∪ {b?}
referenceBook′ = ReferenceBook
borrowers′ = Borrowers ∖ {p?}
sellTo′ = {b?} ⩤ sellTo
r! = BookReceived
m) Report of books on loan: The system can give a report of all books that are currently on loan.
The function report_of_books_onLoan is used to do this task.
Report_of_books_onLoan
Δ Library′
t? : Title
r! : SystemResponse
t? ∈ title ∖ ran lentTo
onShelves′ = onShelves \{t?}
onLoan′ = onLoan ∪ {t?}
books′ = Books
lendingBook′ = LendingBook ∪ {t?}
referenceBook′ = ReferenceBook
r! = Books_onLoan
Example

Report_of_books_onLoan
Δ Library′
t? : SAAD
r! : SAAD on loan
t? ∈ title ∖ ran lentTo
onShelves′ = 5 \{t?}
onLoan′ = 5 ∪ {t?}
books′ = 20
lendingBook′ = 10 ∪ {t?}
referenceBook′ = 10
r! = SAAD on loan
Non-trivial predicate statements
These are statements that are predictable and they can either be true or false. The following are
some of the non-trivial predicate statements, which are related to the library management system.
(Gautam, Saini, 2017)
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
For example,
Book Details ⇒ 20203, Calculus, $50, 230
Librarian Details → John Doe, 1234567, [phone], [e-mail]
Student Details ∃ ⇔ 654123, Marcos, [phone], [e-mail]
Reservation Details ∃ ⇔ short loan, 58866, $10, 654123
References
Belafi, Z. D., Hong, T., & Reith, A. (2019). A library of building occupant behavior models represented in
a standardised schema. Energy Efficiency, 12(3), 637-651.
Gautam, P., & Saini, H. (2017). Non-trivial software clone detection using program dependency
graph. International Journal of Open Source Software and Processes (IJOSSP), 8(2), 1-24.
Pearce, D. J., Utting, M., & Groves, L. (2018, April). An Introduction to Software Verification with Whiley.