Project: Library Management System

Build a complete multi-unit application: a limited private Catalog ADT with ordered maps of books and members, domain exceptions with messages, a contract on insertion, loan rules, and a client that exercises every path — then extend it with suggested exercises.

This project combines the course's core topics — packages, private and limited types, records, Unbounded_String, containers, exceptions with messages, contracts and iteration — into a small but realistic application. Read the specification first: it is the whole contract a client needs.

Design

Library.Catalog is limited private: a catalog is a unique resource that should never be copied accidentally. Book_Id and Member_Id are distinct types derived from Positive, so a member number can never be passed as a book number. The private part uses Ada.Containers.Ordered_Maps (made visible only there with 'private with'), so iteration prints books in Id order. Each rule violation has its own exception with a descriptive message; Add_Book has a precondition. Borrower uses Member_Id'Base so that 0 can mean 'on the shelf'.

• limited private Catalog; distinct Id types. • private with for implementation-only dependencies. • One exception per rule, with messages; Pre on Add_Book.

Code Examples

The client tries valid and invalid operations: lending a lent book, exceeding the loan limit of 2, and an unknown book are refused with named exceptions. After book 1 is returned, Grace can borrow it. Output: Lent book 1 to member 10 Refused (LIBRARY.NOT_AVAILABLE): Programming in Ada 2022 is already lent Lent book 2 to member 10 Refused (LIBRARY.LOAN_LIMIT): Ada already has 2 books Refused (LIBRARY.UNKNOWN_BOOK): book 9 Lent book 1 to member 20 Loans: Ada = 1, Grace = 1 # 1 Programming in Ada 2022 - lent to Grace # 2 Building High Integrity Applications with SPARK - lent to Ada # 3 Concurrent and Real-Time Programming in Ada - on shelf

-- file: library.ads
with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
private with Ada.Containers.Ordered_Maps;

--  A small library-management system: books, members and loans
package Library is

   type Book_Id is new Positive;
   type Member_Id is new Positive;

   Not_Available, Unknown_Book, Unknown_Member, Loan_Limit : exception;

   Max_Loans : constant := 2;

   type Catalog is limited private;

   procedure Add_Book (C : in out Catalog; Id : Book_Id; Title : String)
     with Pre => not Has_Book (C, Id);
   procedure Add_Member (C : in out Catalog; Id : Member_Id; Name : String);

   procedure Lend (C : in out Catalog; Book : Book_Id; To : Member_Id);
   procedure Give_Back (C : in out Catalog; Book : Book_Id);

   function Has_Book (C : Catalog; Id : Book_Id) return Boolean;
   function Is_Lent (C : Catalog; Id : Book_Id) return Boolean;
   function Loans_Of (C : Catalog; Member : Member_Id) return Natural;
   procedure Print (C : Catalog);

private
   type Book is record
      Title    : Unbounded_String;
      Borrower : Member_Id'Base := 0;        --  0 = on the shelf
   end record;

   type Member is record
      Name  : Unbounded_String;
      Loans : Natural :
…

Extension Exercises

1) Add due dates with Ada.Calendar and a function Overdue returning a vector of book Ids. 2) Persist the catalog with Stream_IO and custom 'Write/'Read attributes. 3) Add a Type_Invariant stating that each member's Loans equals the number of books whose Borrower is that member. 4) Make the catalog safe for concurrent use by wrapping it in a protected object. 5) Add AUnit (or Mini_Test) tests for every exception path. 6) Search books by title using Ada.Strings.Fixed.Index with case-insensitive mapping.

• Dates, persistence, invariants, concurrency, tests, search.

type Catalog is private; -- copyable type Catalog is limited private;

Copying a catalog would silently duplicate the library state.

procedure Lend (C : in out Catalog; Book, Member : Positive);

procedure Lend (C : in out Catalog; Book : Book_Id; To : Member_Id);

Distinct Id types make swapped arguments a compile error.

raise Not_Available; -- no context raise Not_Available with Title & " is already lent";

Messages make failures self-explanatory in logs.

Why is Catalog limited? A. Performance B. To prevent accidental copies of unique state C. Required by Ordered_Maps D. For tasks

What does 'private with Ada.Containers.Ordered_Maps;' allow? A. Clients to use Ordered_Maps B. Using the package only in the private part and body C. Nothing D. A private child

Why are the books printed in Id order? A. Insertion order B. Ordered_Maps iterate in key order C. Random D. Sorted explicitly

What prevents passing a Member_Id where a Book_Id is expected? A. Comments B. Distinct derived types C. Preconditions D. Nothing Trace the library project.

Real output: Lent book 1 to member 10 Refused (LIBRARY.NOT_AVAILABLE): Programming in Ada 2022 is already lent Lent book 2 to member 10 Refused (LIBRARY.LOAN_LIMIT): Ada already has 2 books Refused (LIBRARY.UNKNOWN_BOOK): book 9 Lent book 1 to member 20 Loans: Ada = 1, Grace = 1 # 1 Programming in Ada 2022 - lent to Grace # 2 Building High Integrity Applications with SPARK - lent to Ada # 3 Concurrent and Real-Time Programming in Ada - on shelf

-- file: library.ads
with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
private with Ada.Containers.Ordered_Maps;

--  A small library-management system: books, members and loans
package Library is

   type Book_Id is new Positive;
   type Member_Id is new Positive;

   Not_Available, Unknown_Book, Unknown_Member, Loan_Limit : exception;

   Max_Loans : constant := 2;

   type Catalog is limited private;

   procedure Add_Book (C : in out Catalog; Id : Book_Id; Title : String)
     with Pre => not Has_Book (C, Id);
   procedure Add_Member (C : in out Catalog; Id : Member_Id; Name : String);

   procedure Lend (C : in out Catalog; Book : Book_Id; To : Member_Id);
   procedure Give_Back (C : in out Catalog; Book : Book_Id);

   function Has_Book (C : Catalog; Id : Book_Id) return Boolean;
   function Is_Lent (C : Catalog; Id : Book_Id) return Boolean;
   function Loans_Of (C : Catalog; Member : Member_Id) return Natural;
   procedure Print (C : Catalog);

private
   type Book is record
      Title    : Unbounded_String;
      Borrower : Member_Id'Base := 0;        --  0 = on the shelf
   end record;

   type Member is record
      Name  : Unbounded_String;
      Loans : Natural :
…