Name : Jadaun Mahmood
Id : 5121322015
Department : BSSE-7 semester
Submitted To : Ms. Ayesha
Subject : Formal Methods
Design a Z state schema for a simple Library Management System
that manages book borrowing.
Sol:
State Schema
Library
------------------------------
available : P BOOKID
issued : P BOOKID
------------------------------
available ∩ issued = ∅
Operation 1: Borrow a Book
Borrow
-----------------------------------------
ΔLibrary
book? : BOOKID
-----------------------------------------
book? ∈ available
book? ∉ issued
-----------------------------------------
available' = available \ {book?}
issued' = issued ∪ {book?}
Operation 2: Return a Book
Return
-----------------------------------------
ΔLibrary
book? : BOOKID
-----------------------------------------
book? ∈ issued
-----------------------------------------
issued' = issued \ {book?}
available' = available ∪ {book?}
Borrow Limit (More Than 3 Books)
Extended State Schema
Library2
---------------------------------------------------
available : P BOOKID
issued : P BOOKID
borrowed : STUDENT ↔ BOOKID
---------------------------------------------------
available ∩ issued = ∅
ran borrowed = issued
Borrow Book With Limit:
BorrowWithLimit
---------------------------------------------------
ΔLibrary2
s? : STUDENT
book? : BOOKID
---------------------------------------------------
book? ∈ available
#(borrowed[{s?}]) < 3
---------------------------------------------------
available' = available \ {book?}
issued' = issued ∪ {book?}
borrowed' = borrowed ∪ {s? ↦ book?}
Error Schema When Borrow Limit Exceeded
BorrowLimitExceeded
---------------------------------------------------
ΞLibrary2
s? : STUDENT
book? : BOOKID
---------------------------------------------------
#(borrowed[{s?}]) ≥ 3
HOSPITAL MANAGEMENT SYSTEM (Z SCHEMAS)
State Schema
Hospital
-------------------------------------------------------
doctors : P DOCTOR
patients : P PATIENT
appointments : (DOCTOR × PATIENT) ↔ DATETIME
-------------------------------------------------------
∀ d:DOCTOR; p:PATIENT; t:DATETIME •
(d,p) ↦ t ∈ appointments ⇒ d ∈ doctors ∧ p ∈ patients
Operation 1: Add Patient
AddPatient
---------------------------------------------------
ΔHospital
p? : PATIENT
---------------------------------------------------
p? ∉ patients
---------------------------------------------------
patients' = patients ∪ {p?}
doctors' = doctors
appointments' = appointments
Operation 2: Add Doctor
AddDoctor
---------------------------------------------------
ΔHospital
d? : DOCTOR
---------------------------------------------------
d? ∉ doctors
---------------------------------------------------
doctors' = doctors ∪ {d?}
patients' = patients
appointments' = appointments
Operation 3: Book Appointment
BookAppointment
--------------------------------------------------------------
ΔHospital
d? : DOCTOR
p? : PATIENT
t? : DATETIME
--------------------------------------------------------------
d? ∈ doctors
p? ∈ patients
(d?, t?) ∉ dom appointments
--------------------------------------------------------------
appointments' = appointments ∪ { (d?, p?) ↦ t? }
doctors' = doctors
patients' = patients
Operation 4: Cancel Appointment
CancelAppointment
--------------------------------------------------------------
ΔHospital
d? : DOCTOR
p? : PATIENT
t? : DATETIME
--------------------------------------------------------------
(d?, p?) ↦ t? ∈ appointments
--------------------------------------------------------------
appointments' = appointments \ { (d?, p?) ↦ t? }
doctors' = doctors
patients' = patients