ITECH7410: Formal Specification of a Library System

This document presents a formal specification of a library system, developed as part of the ITECH7410 Software Engineering Methodologies course. The specification utilizes the Z-schema notation to formally define the system's data structures and operations. The document begins by outlining the Z-schema for core components such as BookList and BorrowerList, detailing their attributes and relationships. It includes examples demonstrating the system's initial state and how various operations, such as adding books and borrowers, deleting books and borrowers, lending and returning books, and managing reservations, are performed. The document also includes predicate statements to define the constraints and behaviors of the system, ensuring data integrity and consistency. Finally, it provides a bibliography of relevant academic sources. This assignment showcases the application of formal methods in software engineering to create a precise and unambiguous specification of a library system.

Running head: SOFTWARE ENGINEERING AND METHODOLOGIES
Software Engineering and Methodologies
Name of the Student
Name of the University
Author’s note:

1SOFTWARE ENGINEERING AND METHODOLOGIES
Table of Contents
1. Z-Schema:....................................................................................................................................2
2. Examples:....................................................................................................................................5
3. Predicate Statements:...................................................................................................................6
Bibliography:...................................................................................................................................8

2SOFTWARE ENGINEERING AND METHODOLOGIES
1. Z-Schema:
BookList
known: ℙ TITLE
book: TITLE ⇸ AVAILABLECOPY
known = dom book
BorrowerList
known: ℙ NAME
borrower: NAME ⇸ ADDRESS
known = dom borrower
Library
stock: COPY ⇸ BOOK
lent: COPY ⇸ BORROWER
reserved: COPY ⇸ BORROWER
shelved: 𝔽 COPY
bought: 𝔽 COPY
borrowers: 𝔽 BORROWER
∀x: COPY
y1, y2: BORROWER⦁(x↦y)∈issued∧(x↦y2)∈issued ⇒ y1 = y2
shelved ∪domissued=domstock
shelved∩ domissued=∅
ran issued ⊆ borowwers
ran reserved
⊆ borowwers
∀r: borrowers⦁♯(issued ▷{r}) ≤ maxloans
∀r: borrowers
⦁♯(bought
▷{r}) ≤ maxloans
AddBook
Δ BookList
title? : TITLE
availablecopy? : AVAILABLECOPY
title? ∉ known
book′ = book ∪ {title? ⦁ availablecopy?}

3SOFTWARE ENGINEERING AND METHODOLOGIES
addBorrower
Δ BorrowerList
name? : NAME
ADDRESS? : ADDRESS
name? ∉ known
borrower′ = borrower ∪{name?⦁ADDRESS?}
deleteBook
ΔBookList
title? : TITLE
title? ∈ dom book
book′ = {title?} ⩤ book
deleteBorrower
Δ BorrowerList
name? : NAME
name? ∈ dom borrower
borrower′={name?}⩤ borrower
lendBook
ΔLibrary
copy?: COPY
borrower?: BORROWER
copy? ∈ shelved; borrower? ∈ borrowers
♯ (lent ▷ {borrower?} ) < maxloans
lent'= lent⊕{copy? ⇸ borrower?}
stock′ = stock; borrowers′=borrowers
returnBook
ΔLibrary
copy? : COPY
borrower?: BORROWER
copy? ∈ shelved
borrower? ∈ borrowers
lent′ = lent ⊕{copy? ↦ borrower?}
shelved′ = shelved ⇸ {copy?}
stock′ = stock; borrowers′=borrowers

4SOFTWARE ENGINEERING AND METHODOLOGIES
enquireBook
ΞBookList
titile? : NAME
availablecopy! : AVAILABLECOPY
title? ∈ known
availablecopy! = book(titile?)
reserveBook
ΔLibrary
copy?: COPY
borrower?: BORROWER
copy? ∉ shelved
borrower? ∈ borrowers
reserved′ = reserved⊕{copy? ↦ borrower?}
stock′ = stock; borrowers′=borrowers
enquireReservation
ΞLibrary
book? : BOOK
book? : BOOK⦁book∉ dom reserved
copy! = stock(book?)
cancelReservation
ΔLibrary
book? : BOOK
book?
∉ dom reserved
reserved′ = reserved(book?) ⩤ stock
buyBook
ΔLibrary
copy?: COPY
borrower?: BORROWER
copy? ∈ shelved; borrower? ∈ borrowers
♯ (bought ▷ {borrower?} ) < maxloans
bought' = bought ⊕{copy? ⇸ borrower?}
stock′ = stock; borrowers′=borrowers

5SOFTWARE ENGINEERING AND METHODOLOGIES
receiveBooks
ΔLibrary
book?: BOOK ⇸ TITLE
copy?: COPY
availablecopy?: AVAILABLECOPY
newcopy? = NEWCOPY
if
book? ∉ known
then
title? ∉ known
book′ = book ∪ {title? ⦁ availablecopy?}
else
copy?: COPY ∈ dom stock
stock′=stock ⊕ {copy? ↦ book?}
shelved′ = shelved ⇸ {copy?}
availablecopy′ = newcopy
issued′= issued; borrowers′=borrowers
loanReport
ΔLibrary
book? : BOOK
book? : BOOK⦁book∉ dom lent
copy! = stock(book?)
2. Examples:
The library will not have any record of the books or borrower when it is first launched.
BookList
known: ℙ TITLE
book: TITLE ⇸ AVAILABLECOPY
TITLE = ∅
AVAILABLECOPY = ∅
BorrowerList
known: ℙ NAME
borrower: NAME ⇸ ADDRESS
NAME = ∅
ADDRESS = ∅

6SOFTWARE ENGINEERING AND METHODOLOGIES
A new borrower comes to the library to register. The borrower details are recorded into
the system. The name of the borrower is john. known = {John}, address = {John, Main street}
A new book is added to the library with title war and peace. The available copy of the
book is 20. Then known = {War and Peace}, availablecopy = {War and Peace, 20}
If the book is deleted, the booklist schema is updated and the book with title ‘War and
Peace’ is deleted from the system. The address is not entered as one input is enough for deleting
the book.
If a borrower wants to rent a book then both borrower and book details are used. As a
copy of the book is lent to the borrower, the copy resembles one copy of the book. The system
checks of the maximum loan copy is exceeded or not. If copy is available, the system lent the
copy to the borrower.
3. Predicate Statements:
Borrower can borrow books. Books has many copies. Borrower borrows copies.
 The library allows the borrowers rent copies of book. The rent will be available till
one copy is available. If every copies are rented then borrower can reserve a book.
Library can add copies of book. Library can also add book.
 If a book is already available in the library then it adds the number of same books
available in copies and update the available copy. If the book is new then system uses
the addBook function.
The borrower can cancel a reservation. Status of reservation can be checked. A borrower
cancel a reservation by checking status.

7SOFTWARE ENGINEERING AND METHODOLOGIES
 The borrower enter the book which is reserved. The system shows the option of
canceling it. The borrower cancel the reservation. The library system update the
reserved state.

8SOFTWARE ENGINEERING AND METHODOLOGIES
Bibliography:
El Miloudi, K., & Ettouhami, A. (2018). A Multiview Formal Model of Use Case Diagrams
Using Z Notation: Towards Improving Functional Requirements Quality. Journal of
Engineering, 2018.
Gomes, A. O., & Butterfield, A. (2016, May). Modelling the haemodialysis machine with circus.
In International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (pp.
409-424). Springer, Cham.
Grant, E. S., & Brown, T. (2016). Towards Rigorous Transformation Rules for Converting UML
Operation Signatures to Z Schema. In Proceedings of the International MultiConference
of Engineers and Computer Scientists (Vol. 1).
Grant, E. S., Jackson, V. K., & Clachar, S. A. (2018). Towards a Formal Approach to Validating
and Verifying Functional Design for Complex Safety Critical Systems. GSTF Journal on
Computing (JoC), 2(1).
Kaufmann, T., & Weyer, T. (2017). Establishing Role-based Access Control in Viewpoint-
oriented Variability Management. arXiv preprint arXiv:1703.02754.
Rivera, V., Bhattacharya, S., & Cataño, N. (2016, May). Undertaking the tokeneer challenge in
Event-B. In Proceedings of the 4th FME Workshop on Formal Methods in Software
Engineering (pp. 8-14). ACM.
Singh, M., & Jain, V. K. (2017). A New Comment on Reinforcement of Testing
Criteria. INTERNATIONAL JOURNAL OF ADVANCED COMPUTER SCIENCE AND
APPLICATIONS, 8(3), 338-342.

9SOFTWARE ENGINEERING AND METHODOLOGIES
Singh, M., Sharma, A. K., & Saxena, R. (2016). An UML+ Z framework for validating and
verifying the Static aspect of Safety Critical System. Procedia Computer Science, 85,
352-361.
Siregar, M. U. (2016, July). Support for model checking Z specifications. In 2016 IEEE 17th
International Conference on Information Reuse and Integration (IRI) (pp. 241-248).
IEEE.