% 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);
% 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);