Library loan management

The following example shows the loan management of a university library.

A library has a set of books (one copy of each book), each identified by a unique "call number". Books may be loaned to borrowers, who may be faculty members. A book can normally be borrowed for two weeks and two one week extensions are allowed. Some books may be placed on restricted loan; these can only be taken out by faculty members for three days and cannot be renewed. In general, any borrower may have on loan at most five books at any time, and at most one short term loan book.

A preliminary database schema is:

% Load "Date library" %

let ToDay := mkDate(2, 2, 1995);
let type NoRenewals <-> int
            before  mk(this)
            if Not(this >= 0 And this <= 2)
            do failwith "A loan may be renewed only twice";

let rec 
Authors class
    Author <->
        [ FirstName: string;
           LastName: string;
           Nationality :string ]
and
Publishers class
    Publisher <-> 
        [ Name :string;
          Address :string ]
key(Name) 
and
Books class
    Book <->
      [ CallN :int;
        Publisher :Publisher;
        Authors :seq Author;
        Title :string;
        LoanedTo:= meth(theBorrower: Borrower) :Loan is
              (if theBorrower.NOutstandingLoans >= 5
                    then failwith "to many books on loan"
                    else if some Loans with Book = self
                           then failwith "Book not available"
                           else mkLoan(
                                  [Book := self;
                                    LoanedTo := theBorrower;
                                    DueDate := 
                                       var (ToDay.AddDays(14));
                                    RenewalsLeft := var mkNoRenewals(2)                      
                                   ]     )
               )        
       ]        
key(CallN)
and
 Borrowers class 
    Borrower <->
       [ Name :string;
         Address :var string;
         BooksBorrowed := meth() : seq [Book :Book; 
                                        DueDate :Date; 
                                        RenewalsLeft :NoRenewals] is
                select[ Book := Book;
                        DueDate := at DueDate;
                        RenewalsLeft := at RenewalsLeft ]
                from Loans where LoanedTo = self; 
          NOutstandingLoans := meth() :int is count(Loans where LoanedTo = self)
        ]                   
and
Loans class
    Loan <->
      [ Book :Book;
        LoanedTo :Borrower;
        DueDate :var Date;
        RenewalsLeft : var NoRenewals] 
key(Book);

% Data %

let a1 := mkAuthor([FirstName := "joe"; LastName := "stoy"; 
                     Nationality := "American"]);
let a2 := mkAuthor([FirstName := "jim"; LastName := "jen"; 
                     Nationality := "American"]);
let a3 := mkAuthor([FirstName := "nik"; LastName := "wir"; 
                     Nationality := "Swiss"]);
let e1 := mkPublisher( [Name :="sw"; Address := "b" ] );
let e2 := mkPublisher( [Name :="aw"; Address := "nj" ] );
let b1 := mkBook([ CallN := 1; Publisher := e1; Authors := {a2;a3}; 
                    Title := "pa" ]);
let b2 := mkBook([ CallN := 2; Publisher := e2; Authors := {a1};
                    Title := "ds" ]);
let u1 := mkBorrower( [Name :="aa"; Address := var "di"] );
let u2 := mkBorrower( [Name :="rb"; Address := var "di"] );

b1.LoanedTo(u1);
b2.LoanedTo(u2);

The database schema is then refined by specialization in the following way:

%  Schema refinement %

let rec
ComputerBooks subset of Books class
  ComputerBook <-> is Book and 
     [ Publisher: SciencePublisher;
       CRSubjectCode :seq string]
and
ShortTermLoanBooks subset of Books class        
  ShortTermLoanBook <-> is Book and 
     [ ExpiryOfRestriction : Date;
       LoanedTo:= 
          meth(theBorrower: Borrower) :Loan is
           if Not theBorrower isalso FacultyMember
            then failwith "Loan for FacultyMembers"
            else 
              if (theBorrower As FacultyMember).HasShortLoan
                then failwith "One ShortTermLoanBook only is allowed"
                else 
                use ALoan:= 
                       ((self As Book)!LoanedTo) (theBorrower)
                 in  (ALoan.RenewalsLeft <- mkNoRenewals(0);
                      ALoan.DueDate 
                                  <- ToDay.AddDays(3);    
                      ALoan 
                      )
      ]     
and
SciencePublishers subset of Publishers class
  SciencePublisher <-> is Publisher and [ ]
and
FacultyMembers subset of Borrowers class
  FacultyMember <-> is Borrower and
         [ Phone : string;
           HasShortLoan := meth() :bool is
               some x In Loans with (x.LoanedTo = self) 
                And (x.Book isalso ShortTermLoanBook)
          ];

let se1:= inSciencePublisher(e1, [ ]);
let sb1:= inComputerBook(b1,[Publisher := se1;
                             CRSubjectCode := {"Programming Language"}     
                             ]);
let d1:= inFacultyMember(u1, [Phone := "887266"]);
let b3:= mkShortTermLoanBook
            ([ CallN:=3;
               Publisher:= 
                 mkPublisher([Name := "Oxford University Press";
                             Address := "Oxford"]);
               Authors := {mkAuthor([FirstName := "A S";
                                     LastName:="Hornby";
                                     Nationality := "English" ]) };
               Title := "Oxford Dictionary of Current English";
               ExpiryOfRestriction:= mkDate(31, 12, 1996)
            ]);

b3.LoanedTo(d1);