Guide to Project for Supervisors CRICOS Provider No. 00103D ITECH7410 Assignment XXXXXXXXXXGroup Page 1 of 3 ITECH7410 Software Engineering Methodologies Assignment 2 – Group Formal Specification of a...

Library System Specification
Student Name
Student Id
Contents
Abstract                                3
Schema for the functions                    4
Add a book                        4
Add a borrower                        5
Delete a book                        5
Delete a borrower                    6
Lend a book                        6
Return book                        7
Enquire about the book                8
Reservation for a book                8
Enquire about the reservation             9
Cancel reservation                 10
Buy new book                    11
Receive new book                    11
Report of books on loan                12
Schema examples                        12
Z annotation                         16
Non-trivial predicate statements            17
Abstract
This project is to understand the fundamentals of schema and z annotations. This assignment is a part of Software Engineering methodologies 7410. This report is prepared by Syed ali gohar gilani and Yahya Khan.
This report consists of how a library works. There are 13 functions which are included in this report. We divided these 13 functions among us and all of us contributed equally in this project. Yahya Khan got the responsibility to explain the first 6 functions which are to add book, add borrower and many other actions. Rest of the functions were completed by Syed ali gohar gilani. The functions were to reserve a book, about the reservation and also the report the books bought on loan. The non-predicate statements were explained by both of us as per the functions.
We would like to thank our coordinator for providing us this task. This assignment helped us a lot in understanding about the schemas in detail. We studied from different sources to understand this concept.
1. State space for the given functions (10)
    Book    
bookTitle: P.TITLE
bookAuthor: P.AUTHOR
bookEdition:P.EDITION
bookISBN: P.ISBN
bookPublisher: P.PUBLISHER
bookDetail:{Title⦁Edition}⦁Author⦁ISBN⦁PUBLISHER
bookName=dom bookDetail
    
    Borrower    
borrowerName:PNAME
borrowerPhoneNo:PBORROWER_PHONENO
borrowerMemID:PBORROWER_MEMID
borrowed: (Name⦁BORROWER_MEMID)⦁bookDetail
Borrower=dom borrowed

    Reservation    
memberName:NMEMBERNAME
memberId:NMEMBER_ID
reserve: (Name⦁Member_id)⦁bookDetail
member=dom reservation
1.1. Add a book
    AddBook    
ΔBook
book_name?:NAME
book_edition?:EDITION
book_author?:AUTHOR
book_ISBN?:ISBN    
info!:ALERT
book_name?∉book_Name
bookDetail?=bookDetail ∪ {book_Name?↦book_Edition?↦book_Author? ↦book_ISBN?}
info!: ′Book added successfully′
    ErrorAddBook    
ΞBook
book_name?:NAME
info!:ALERT
book_name?∈bookName
info!=′Book already exists′
1.2. Add a borrower
    AddBorrower    
ΔBorrower
borrowerName?: NAME
borrowerMemId?: BORROWER_MEMID
info!:ALERT
borrower?∉borrowerName
borrowed′ =borrowed ∪ {borrowerName ↦borrowerMemID?}
info!=′Added to borrowed list′
    Error    
ΞBorrower
borrower?:BORROWER_NAME
borrowerMemId?: BORROWER_MEMID
info!:ALERT
borrower?∉ borrower∧borrowerMemId?∉borrowerMemId
info!=′Borrower can’t be added in the list′
1.3. Delete a book
    DeleteBook    
ΔBook
Book_Name?:NAME
Book_Author?:AUTHOR
Book_ISBN?:ISBN
info!=′ALERT
book?∉bookName
author?∉bookAuthor
book_ISBN?∉bookISBN
delBook=bookName∖{book? ↦book_Author? ↦book_ISBN?}
info!=′Book is removed from the list′
    ErrorDeleteBook    
ΞBook
Book_Name?:NAME
Book_Author?:AUTHOR
Book_ISBN?:ISBN
info!=ALERT
book?∉bookName
author?∉bookAuthor
book_ISBN?∉bookISBN
info!=′Book can’t be deleted′
1.4. Delete a borrower
    DeleteBorrower    
ΔBorrower
borrower?:BORROWER
borrower?:BORROWER_MEMID
info!:ALERT
borrower?∈borrowerName
borrower?∉borrower_MemId
borrower?∉borrower_EmailId
delBorrower=borrowerName∖{person? ↦ borrower_MemId? ↦ borrower_EmailId?}
info!=′Borrower deleted successfully′
    Error    
ΞBorrower
borrower?:PERSON
info!:ALERT
borrower?∉borrowerName
borrower?∉borrower_MemId
info!=′Unable to delete borrower′
1.5. Lend a book to a borrower
    Lend    
lendBookDetail:Book
lendId:LEND_ID
borrowerName:BORROWER_NAME
borrowerMemID:BORROWER_MEMID
issuedate:ISSUE_DATE
lendDetail:{lendId⦁lendBookDetail}⦁issuedate
borrowerDetail:borrowerName⦁borrowerMemID
lendDetail=dom borrowerDetail
    LendBook    
ΔBook
issueBook:?:BOOK
lID?:LENDI_ID
bID?:BORROWER_MEMID
bookBorrower?:PERSON
date?:DATE
info!:′ALERT′
issueBook?∉bookDetail
bookDetail′=bookDetail∖{ issueBook?}
borrowed′=borrowed ∪ { issueBook?↦bookBorrower?}
info!=′Successfully book lended′
    Error    
ΞBook
issueBook?:BOOK
info!=ALERT
issueBook?∉bookDetail
info!=′Book issueing was unsuccessful′
1.6. Return a book from a borrower
ReturnBook    
ΔBook
returnBook?:BOOK_DETAIL
returnBorrow?:BORROWER_DETAIL
info!:ALERT
(returnBook?↦returnBorrow?)∈borrowed
bookDetail′=bookDetail ∪ {returnBook?}
borrowed′=borrowed∖{returnBorrow?}
info!=′Book returned′
    Error    
ΞBook
returnBook?: BOOK_DETAIL
returnBorrow?:BORROWER_DETAIL
info!:ALERT
(returnBook?↦returnBorrow?)∉borrowed
info!=′Book returning failed′
1.7. Enquire about a book
    EnquiryBook    
ΞBook
bookname?:BOOK_NAME
bookedition?: BOOK_EDITION
bookauthor?: BOOK_AUTHOR
bookpublisher?: BOOK_PUBLISHER
name?∈bookName
edition!=bookDetail(edition?)
author!=bookDetail(author?)
publisher!=bookDetail(publisher?)
    Error    
ΞBook
name?:NAME
info!:ALERT
name?:∉bookName
info!=′Book enquiry failed′
1.8. Reserve a book
ReservationAddition    
ΔReservation
bookName?:BOOK_NAME
bookEdition?: BOOK_EDITION
bookAuthor?: BOOK_AUTHOR
bookpublisher?: BOOK_PUBLISHER
r_bookDetail?:{ BOOK_NAME⦁ BOOK_EDITION}⦁ BOOK_AUTHOR⦁...