This repository contains every artefact produced for the development of a simplified Library Management System specified with Z Notation, prototyped in Python, and implemented for the Java Virtual Machine (CLI).
The project demonstrates, end‑to‑end, the application of formal specification techniques to real software development.
- Apply Formal Methods (Z Notation) to specify a real‑world problem.
- Evolve the system through the following stages: requirements, formal spec, Python behavioural model, Java implementation and testing.
- Register new users and books.
- Add copies to the stock of a book.
- Loan an available book.
- Reserve an unavailable book.
- Record book ratings, reviews and purchase requests.
- Manage user subscription plans and send notifications.
- Desktop application written for the JVM.
- Command‑line interface (CLI) covering all functional operations.
The specification defines:
- Abstract types:
Usuario,Livro,Plano,Resenha,Mensagem, - State variables: sets, relations and functions such as
usuarios,livros,estoque,emprestimos,reservas,assinaturas,pedidos,resenhas,notificacoes. - Ten operations: from CadastrarUsuario to CriarNotificacao, each with precise pre‑ and post‑conditions.
Section 5 of the report presents a line‑for‑line Python model that mirrors the Z operations, used to validate the specification before coding in Java.
- Conforms to the JVM and provides a command‑line interface (RNF 1–3).
- Maps each Z operation to an equivalent Java method (section 6.2).
- Fully tested with JUnit to ensure state transitions follow the formal spec.
| Nº | Nome |
|---|---|
| 1 | Anne Yumi Kagawa |
| 2 | Cinthia Alves Barreto |
| 3 | David Mendes Saldanha de Miranda |
| 4 | Igor Gabriel Santos Simões |
| 5 | Isabella Rubio Venancio |
| 6 | Joao Murilo de Amorim Mariano Santos |
| 7 | João Pedro Grinover Borgneth |
| 8 | Leonardo Fajardo Grupioni |
| 9 | Matheus Ferreira dos Santos Silvestre |
| 10 | Rodrigo Poinha Romero |
| 11 | Steven She Cheng Wang |
Course: Formal Methods, Computer Science – PUC‑SP 2025
Material provided for academic reference.