ITECH7410: Group Project - Formal Specification of Library System

This document presents a formal specification of a library system developed as a group project for the ITECH7410 Software Engineering Methodologies course. The specification utilizes Z notation to define the system's functionality, including adding books, borrowers, and handling operations like borrowing, returning, and reserving books. The assignment includes detailed Z schema for various operations, such as adding and deleting books and borrowers, and also includes a demonstration of the system's functions. The document also features annotations of Z statements, non-trivial predicate statements, and a bibliography of relevant sources. The project emphasizes the application of formal methods to improve the accuracy and reliability of software systems, particularly in the context of library management. The student has used formal methods for software development and the Z notation is used as a formal technique for improving the accuracy of the execution of the functionality.

Running head: ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
ITECH7410 Software Engineering Methodologies
Name of the Student
Name of the University
Author’s Note

1ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Abstract
For the development of the Z scheme was to complete the task on time by organizing the task.
For the completion of the task it was divided into sub parts and time was allocated for
completion of each of the task.
A formal specification is prepared for a library management system with the application of Z
schema. The writing part of Z notation and explanation of predicate is done by student1 and the
other part like derivation of functionality is done by student2.
The task is based on library management system and for the development of the Z schema the
functionality of the system is analyzed. The Z notation is used as a formal technique for
improving the accuracy of the execution of the functionality and utilization of formal strategies
for the development of the programming framework.

2ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Table of Contents
Functionality....................................................................................................................................3
Demonstration of the System.........................................................................................................10
Annotation of Z statement for the schema.....................................................................................14
Non-trival predicate statement.......................................................................................................17
Bibliography..................................................................................................................................19

3ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Functionality
Add a book
LibrarySystem
name? : BOOK
rep! : MESSAGE
----------------------------
name? 6∈book
book ′ = book ∪ {name?}
directory ′ = directory
rep! = ‘OK’
If book exists
BookExists
ΞLibrarySystem
name? : Book
rep! : MESSAGE
---------------------------
name? ∈ book
rep! = ‘Book already exists’

4ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Add a borrower
AddBorrowerOK
LibrarySystem
name? : Borrower
b?:BOOK
number ? : PHONE
-----------------------------
rep! : MESSAGE
name? ∈ borrower
name? number ? 6∈directory
directory ′ = directory ∪ {name? number ?} borrower ′ =borrower
rep! = ‘DONE’
Delete a book
RemoveBook
LibrarySystem
name? : BOOK
rep! : MESSAGE
---------------------------

5ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
name? ∈ book
book ′ = book \ {name?}
directory ′ = {name?} −⊳ directory
rep! = ‘OK’
Delete a borrower
RemoveBorrower
LibrarySystem
name? : BORROWER
rep! : MESSAGE
-----------------------------
name?
∈ borrower
borrower ′ = borrower \ {name?}
directory ′ = {name?} −
⊳ directory
rep! = ‘OK’
Return a book from a borrower
RetunBookOK
availablebook, availablebook′ : B BOOK
borrowedbook , borrowedbook′ : BOOK 7→USERNAME

6ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
--------------------------------------------------------------------------------
availablebook ∪ dom borrowedbook = BOOK
availablebook ∩ dom borrowedbook = ∅
availablebook′ ∪ dom borrowedbook ′ = BOOK
availablebook′ ∩ dom borrowedbook ′ = ∅
Ξ LibrarySystem Ξ LibrarySystem=b
[LibrarySystem | borrowedbook ′ = borrowedbook ∧ availablebook′ = availablebook
Enquire about a book
FindBooksOk
Ξ LibrarySystem
names! : B BOOK
rep! : MESSAGEAPP
----------------------------------------------------
number ?
∈ ran directoryname
names! = directory name−1 (| {number ?} |)
rep! = ‘DONE’
Reserve a book
LibrarySystem

7ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
b? : BOOK
------------------------------
B? 6∈Books
books′ = books ∪ {b?}
Enquire about a reservation
EnquiryBookReservation
ΞLibrarySystem
names! : B BOOK
r!:ReserveBook
rep! : MESSAGEAPP
---------------------------------------------
number ? ∈ ran directory
names! = directory −1 (| {number ?} |)
rep! = ‘DONE’
Cancel a reservation
CancelReserveBook
LibrarySystem
b? : BOOK

8ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
------------------------------------------
B? 6∈Books
books′ = books
∪ {b?}
names! = directory −1 (| {number ?} |)
rep! = ‘OK’
Buy a book
BuyBookOK
LibrarySystem
u? : USERNAME
b? : BOOKNAME
rep! : MESSAGEAPP
------------------------------------------------
b?
∈ availablebook
availablebook′ = availablebook \ {b?}
rep! = ‘DONE’
Receive a book
RecBookOK
LibrarySystem

9ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
u? : USERNAME
b? : BOOKNAME
rep! : MESSAGEAPP
----------------------------------------------------------------
b? ∈ availablebook
availablebook′ = availablebook \ {b?}
borrowedbook ′ = borrowedbook ∪ {b? u?}
rep! = ‘DONE’
Report of books on loan
RecBookOK
LibrarySystem
u? : USERNAME
b? : BOOKNAME
rep! : MESSAGEAPP
---------------------------------------------------------
b? ∈ availablebook
availablebook′ = availablebook \ {b?}
borrowedbook ′ = borrowedbook ∪ {b? u?}

10ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
rep! = ‘DONE’
Demonstration of the System
Add books
Add a borrower
Delete a book

11ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Delete a borrower
Lend a book to a borrower
Return a book from a borrower