ITECH7410 Software Engineering: Formal Specification of Library System

This assignment presents a formal specification of a library system using the Z-schema notation. It defines the system's state, including books, members, stock, and loans, along with operations such as adding books and members, lending and returning books, making reservations, and handling purchases. The specification includes schemas for various operations, pre- and post-conditions, and examples illustrating the system's initial state and behavior. Predicate statements outline the rules governing member borrowing and book availability. The document also provides a bibliography of relevant resources. Desklib is a platform where students can find this and similar assignments.

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:...................................................................................................................................7

2SOFTWARE ENGINEERING AND METHODOLOGIES
1. Z-Schema:
Books
known: ℙ TITLE
book: TITLE ⇸ INSTOCK
known = dom book
MemberList
known: ℙ NAME
member: NAME ⇸ CONTACT
known = dom member
Library
stock: COPY ⇸ BOOK
lent: COPY ⇸ MEMBER
reserved: COPY ⇸ MEMBER
shelved: 𝔽 COPY
purchased: 𝔽 COPY
members: 𝔽 MEMBER
∀x: COPY
y1, y2: MEMBER⦁(x↦y)∈issued∧(x↦y2)∈issued ⇒ y1 = y2
shelved ∪domissued=domstock
shelved∩ domissued=∅
ran issued ⊆ borowwers
ran reserved
⊆ borowwers
∀r: members⦁♯(issued ▷{r}) ≤ maxloans
∀r: members
⦁♯(purchased
▷{r}) ≤ maxloans
AddBook
Δ Books
title? : TITLE
INSTOCK? : INSTOCK
title? ∉ known
book′ = book ∪ {title? ⦁ INSTOCK?}

3SOFTWARE ENGINEERING AND METHODOLOGIES
addMember
Δ MemberList
name? : NAME
CONTACT? : CONTACT
name? ∉ known
member′ = member ∪{name?⦁CONTACT?}
deleteBook
ΔBooks
title? : TITLE
title? ∈ dom book
book′ = {title?} ⩤ book
deleteMember
Δ MmeberList
name? : NAME
name? ∈ dom member
member′={name?}⩤ member
lendBook
ΔLibrary
copy?: COPY
member?: MEMBER
copy? ∈ shelved; member? ∈ members
♯ (lent ▷ {member?} ) < maxloans
lent'= lent⊕{copy? ⇸ member?}
stock′ = stock; members′=members
returnBook
ΔLibrary
copy? : COPY
member?: MEMBER
copy? ∈ shelved
member? ∈ members
lent′ = lent ⊕{copy? ↦ member?}
shelved′ = shelved ⇸ {copy?}
stock′ = stock; members′=members

4SOFTWARE ENGINEERING AND METHODOLOGIES
enquireBook
ΞBooks
titile? : NAME
INSTOCK! : INSTOCK
title? ∈ known
INSTOCK! = book(titile?)
reserveBook
ΔLibrary
copy?: COPY
member?: MEMBER
copy? ∉ shelved
member? ∈ members
reserved′ = reserved⊕{copy? ↦ member?}
stock′ = stock; members′=members
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
member?: MEMBER
copy? ∈ shelved; member? ∈ members
♯ (purchased ▷ {member?} ) < maxloans
purchased' = purchased ⊕{copy? ⇸ member?}
stock′ = stock; members′=members

5SOFTWARE ENGINEERING AND METHODOLOGIES
receiveBooks
ΔLibrary
book?: BOOK ⇸ TITLE
copy?: COPY
INSTOCK?: INSTOCK
newcopy? = NEWCOPY
copy?: COPY ∈ dom stock
stock′=stock ⊕ {copy? ↦ book?}
shelved′ = shelved ⇸ {copy?}
INSTOCK′ = newcopy
issued′= issued; members′=members
loanReport
ΔLibrary
book? : BOOK
book? : BOOK⦁book∉ dom lent
copy! = issued(book?)
2. Examples:
When the system will be deployed in the library environment it will not have any data of
member or books
Books
known: ℙ TITLE
book: TITLE ⇸ INSTOCK
TITLE = ∅
INSTOCK = ∅
MemberList
known: ℙ NAME
member: NAME ⇸ CONTACT
NAME = ∅
CONTACT = ∅
Taken as an example, a new member sends request to join the library as member. The
name of the member is john. known = {Mark}, CONTACT = {037-056 877}

6SOFTWARE ENGINEERING AND METHODOLOGIES
The books are needed to be added to library so that member can borrow it. Taken as an
example a new book to be added to library has 100 copies. Then known = {Le Miserable},
INSTOCK = { Le Miserable, 100}
3. Predicate Statements:
Members are allowed borrow books. Members can borrow one copy at a time. Member
will return the borrowed copy to re-issue it.
 Library record the lending of books along with the member who rents it and the
return details.
Library has books. Copy of books are rented and sold to members. Members can rent or
buy single copy of book at a time.
 The system will record the book copy number and member detail when renting copy
of book. If the book is not available then system reject request.
Member make reservation of books. The reservation is made using book title. The
member make reservation for a book not its copy.
 If member cannot find the book in the library then he/she can add the book to
registration. Therefore, if any copy of the book is available, the member will be
notified.

7SOFTWARE ENGINEERING AND METHODOLOGIES
Bibliography:
Bowen, J. P. (2016). The Z Notation: Whence the Cause and Whither the Course?.
In Engineering Trustworthy Software Systems (pp. 103-151). Springer, Cham.
Pandey, T., & Srivastava, S. (2015). Comparative Analysis of Formal Specification Languages
Z, VDM and B. International Journal of Current Engineering and Technology, 5(3),
2086-2091.