scheme implicit=
class
type 	
Author= Text,
Title = Text,
Available = Nat,
QTY= Nat,
Book = Title >< Author,
BookInfo = Book >< Available >< QTY,
Catalog = BookInfo-set,
Name = Text,
Surname = Text,
Reader = Name >< Surname,
BookList = Book-set,
ReaderInfo = Reader >< BookList,
Visitors = ReaderInfo-set,    
Library = Catalog >< Visitors

value
	IsBook : Book >< Library -> Bool
	IsBook (B,(C,V)) as Flag
	post
	Flag = ( exists (b,a,q) : BookInfo :- (b,a,q) isin C /\ b=B ),
		
	GetAvailable : Book >< Library -> Available
	GetAvailable (B,(C,V)) as N
	post
	if IsBook(B,(C,V)) then
		(exists (b,a,q):BookInfo :- (b,a,q) isin C /\ b=B /\ a=N)
	else
		N=0
	end,

	GetQTY : Book >< Library -> QTY
	GetQTY (B,(C,V)) as N
	post
	if IsBook(B,(C,V)) then
		(exists (b,a,q):BookInfo :- (b,a,q) isin C /\ b=B /\ q=N)
	else
		N=0
	end,

	IsReader : Reader >< Library -> Bool
	IsReader (R,(C,V)) as Flag
	post
	Flag = (exists (r,bs) : ReaderInfo :- (r,bs) isin V /\ r=R),
		
	HaveABook: Book >< Reader >< Library -> Bool
	HaveABook (B,R,(C,V)) as Flag
	post
	Flag = (exists (r,bl):ReaderInfo :- r=R /\ B isin bl /\ (r,bl) isin V)
	pre IsReader(R,(C,V)) /\ IsBook(B,(C,V)),

	BookInfoByBook: Book >< Library -> Catalog
	BookInfoByBook (B,(C,V)) as Cat
	post
	(all (b,a,q) : BookInfo :- (b,a,q) isin Cat /\ b=B)
	pre IsBook(B,(C,V)),

	ReaderInfoByReader: Reader >< Library -> Visitors
	ReaderInfoByReader (R,(C,V)) as Vis
	post
	(all (r,bs) : ReaderInfo :- (r,bs) isin Vis /\ r=R)
	pre IsReader (R,(C,V)),

	AddBook : Book >< Library >< Nat-> Library
	AddBook (B,(C,V),c) as Lib
	post
	GetQTY(B,(C,V)) = GetQTY(B, Lib)-c,

	DeleteBook : Book >< Library >< Nat -> Library
	DeleteBook(B,(C,V),c) as Lib
	post
	GetQTY(B,(C,V)) = GetQTY(B, Lib)+c,
	
	AddReader : Reader >< Library -> Library
	AddReader (R,(C,V)) as Lib
	post
	IsReader(R,Lib)
	pre ~IsReader(R,(C,V)),

	GetReaderBooks : Reader >< Library -~-> BookList
	GetReaderBooks (R,(C,V)) as BList
	post
	(all b : Book :- HaveABook(b,R,(C,V)) /\ b isin BList)
	pre IsReader(R,(C,V)),

	DeleteReader : Reader >< Library -> Library
	DeleteReader (R,(C,V)) as Lib
	post
	~IsReader(R,(C,V))
	pre
	IsReader(R,(C,V)),

	GiveBook: Book >< Reader >< Library -~-> Library
	GiveBook (B,R,(C,V)) as (CC,VV)
	post
	GetAvailable(B,(C,V)) = GetAvailable(B,(CC,VV))-1 /\
		GetQTY(B,(C,V)) = GetQTY(B,(CC,VV))
	pre GetAvailable(B,(C,V))>0 /\ IsReader(R, (C,V)) /\ B ~isin GetReaderBooks (R, (C,V)),

	ReturnBook: Book >< Reader >< Library -~-> Library
	ReturnBook (B,R,(C,V)) as (CC,VV)
	post
	GetAvailable(B,(C,V)) = GetAvailable(B,(CC,VV))+1 /\
		GetQTY(B,(C,V)) = GetQTY(B,(CC,VV))
	pre IsReader(R, (C,V)) /\ B isin GetReaderBooks (R, (C,V))

end