Formal Specification: Library System Z Schema, ITECH7410

This assignment presents a comprehensive Z schema for a library system, designed to model and specify its functionalities. The Z schema, a formal specification language, is used to describe the system's operations, including adding and deleting books, managing borrowers, lending books, and handling reservations. The document details the user-defined types, free types, and state spaces within the Z schema, providing a structured approach to representing the library's data and operations. The functionalities include adding, deleting, lending, and returning books, as well as enquiring about books and reservations. The assignment emphasizes the consistency of the Z schema with a standard library system, highlighting predicates that define relationships between books, borrowers, and loan dates. In conclusion, the Z schema offers a clear and concise method for specifying system behavior, enabling modifications and improvements to the library management system. The document references key literature and provides a complete Z schema-based representation of the library system and its tasks. The assignment is a complete solution for ITECH7410 Software Engineering Methodologies assignment 2.

Software Testing
Z SCHEMA: LIBRARY SYSTEM

Introduction
 The Z notation also known as the Z
schema is a formal specification language
that is mainly used for modelling computer
systems and describing them. This
notation is targeted toward the clear
specification of computer based system in
general and computer programs.
 The Z schema is designed based on the
standard mathematical notation that is
used in the axiomatic set theory, first
order predicate logic and lambda calculus.
 The expressions in the Z notation are
typed.

background of library system
 The library system is a system that
can be used to perform the functions
of the library. Some of the core
functions of this library include:
 1. Adding a book
 2. Delete a book
 3. Add a borrower
 4. Return a borrowed book
 5. Reserve a book.

background of library system
(continued)
 6. Cancel a reservation
 7. Receive a book
 8. Buy a book
 9. Enquire for a book
 10. Delete a borrower
 11. Lend a book
 12. Report loaned books

z schemas
 The Z schema notations for the library system can be divided into two
three parts. These parts are:
 1. User defined types:
 [BORROWERID,RESERVATIONID,PHONE_NUM,LENDID,BOOKID,DATE]
 2. Free types:
 STATUS ::= AVAILABLE | SOLD | WAITING | CANCELLED | LEND
 REPORT::= SUCCESS | BOOK_NOT_KNOWN | BORROWER_NOT_KNOWN
| BORROWER_ALREADY_KNOWN | BOOK_NOT_KNOWN

z schemas (continued)
 3. Start spaces
 A. Book
 B. Borrower
 C. Lend
 D. Reservation

z schemas (continued)
 4. Error handling
 A. Success
 B. Already_known_book
 C. Already_known_borrower
 D. Not_Known_Book
 E. Not_Known_Borrower
 F. Book_Not_Available

Functionality
 The main functionalities of the
system are:
 1. Add a book
 2. Add a borrower
 3. Delete a book
 4. Delete a borrower
 5. Lend a book to a borrower

Functionality (continued)
 6. Return a book from a borrower
 7. Enquire about a book
 8. Reserve a book
 9. Enquire about a reservation
 10. Cancel a reservation
 11. Buy a Book
 12. Report of Books on Loan

Consistency with the library
system
 The library system developed
using the Z schema has all the
functions of a normal library. A
normal library has functions like
lend a book, retrieve a book,
record borrower, add borrower,
delete borrower, etc.

Predicates
 The predicates of the library system are:
 1. lends, borrower(x)
 When you book that is lend there is always a borrower. This statement is
always true.
 2. lend, book(x)
 For every person who is lend a book, there is always a book. This statement is
also true.
 3. lend, borrowDate(x)
 For every book lend, there is always a borrower date. This statement is again
true.

Conclusion
 To conclude, the Z schema is a system or a set
of notations to demonstrate the functioning of
a system be it a library management system or
a ticket booking system. The normal tasks
carried out in the system is implemented
electronically via expressions in a Z schema.
 It provides the users with the ability to make
changes or improve the system by making
changes in the notations and upgrading the
system as per requirement.
 The library management system in this report
has been completely denoted via the Z schema
and its tasks are clearly shown with the help of
expressions.