scheme explicit=
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
	Nats: Nat-inflist
axiom
	Nats(1)=0,
	all i: Nat :- i>=2 => Nats(i)=Nats(i-1)+1

value
	IsBook : Book >< Library -> Bool
	IsBook (B,(C,V)) is
	( exists (b,a,q) : BookInfo :- (b,a,q) isin C /\ b=B),
		
	GetAvailable : Book >< Library -> Available
	GetAvailable (B,(C,V)) is
	if IsBook(B,(C,V)) then
		<.n | n in Nats :- all (b,a,q): BookInfo :- (b,a,q) isin C /\ b=B /\ n=a.>(1)
	else
		0
	end,

	GetQTY : Book >< Library -> QTY
	GetQTY (B,(C,V)) is
	<.n | n in Nats :- all (b,a,q): BookInfo :- (b,a,q) isin C /\ b=B /\ n=q.>(1)
	pre IsBook(B,(C,V)),

	IsReader : Reader >< Library -> Bool
	IsReader (R,(C,V)) is
	( exists (r,bs) : ReaderInfo :- (r,bs) isin V /\ r=R),
		
	HaveABook: Book >< Reader >< Library -> Bool
	HaveABook (B,R,(C,V)) is
	(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)) is
	{(b,a,q) | (b,a,q) : BookInfo :- (b,a,q) isin C /\ b=B}
	pre IsBook(B,(C,V)),

	ReaderInfoByReader: Reader >< Library -> Visitors
	ReaderInfoByReader (R,(C,V)) is
	{(r,bs) | (r,bs) : ReaderInfo :- (r,bs) isin V /\ r=R}
	pre IsReader (R,(C,V)),

	AddBook : Book >< Library >< Nat-> Library
	AddBook (B,(C,V),c) is 
	if  ( GetQTY( B,(C,V)) > 0)  
	then ( C \ {(b,a,q) | (b,a,q) : BookInfo :- (b,a,q) isin C /\ b=B} union { (B,newa,newq) | (B,newa,newq) : BookInfo :- newq = c + GetQTY(B,(C,V)) /\ newa= c + GetAvailable(B,(C,V)) } , V )
	else ( C union {(B,c,c) : BookInfo},V)
	end,

	DeleteBook : Book >< Library >< Nat -> Library
	DeleteBook(B,(C,V),c) is
	if  ( c < GetAvailable (B,(C,V)))
	then (C \ {(b,a,q) | (b,a,q) : BookInfo :- (b,a,q) isin C /\ b=B} union {(B,newa, newq) | (B,newa,newq) : BookInfo :- newq = GetQTY(B,(C,V))-c /\ newa=GetAvailable(B,(C,V))-c},V)
	else (C \ {(b,a,q) | (b,a,q) : BookInfo :- (b,a,q) isin C /\ b=B} union {(B,newa, newq) | (B,newa,newq) : BookInfo :- newq = GetQTY(B,(C,V))-GetAvailable(B,(C,V)) /\ newa=0},V)
	end
	pre GetQTY(B,(C,V)) >0 /\ c>0,
	
	AddReader : Reader >< Library -> Library
	AddReader (R,(C,V)) is 
	(C,V union {(R,{})})
	pre  ~IsReader(R,(C,V)),

	GetReaderBooks : Reader >< Library -~-> BookList
	GetReaderBooks (R,(C,V)) is
	{b | b : Book :- HaveABook(b,R,(C,V))}
	pre IsReader(R,(C,V)),

	DeleteReader : Reader >< Library -> Library
	DeleteReader (R,(C,V)) is 
	(C, V \ { (R,GetReaderBooks(R,(C,V))) } )
	pre  IsReader (R,(C,V)) /\ GetReaderBooks(R,(C,V)) = {},

	GiveBook: Book >< Reader >< Library -~-> Library
	GiveBook (B,R,(C,V)) is 
	(C \ {(	B,GetAvailable(B,(C,V)), GetQTY(B,(C,V))) : BookInfo} union {(B,GetAvailable (B, (C,V))-1, GetQTY (B, (C,V))) : BookInfo}, V \ {(R,GetReaderBooks(R,(C,V))) : ReaderInfo} union {(R,GetReaderBooks(R, (C,V)) union {b | b : Book :- b=B}) : ReaderInfo})
	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)) is 
	(C \ {(	B,GetAvailable(B,(C,V)), GetQTY(B,(C,V))) : BookInfo} union {(B,GetAvailable (B, (C,V))+1, GetQTY (B, (C,V))) : BookInfo}, V \ {(R,GetReaderBooks(R,(C,V))) : ReaderInfo} union {(R,{b|b:Book:-b isin GetReaderBooks(R, (C,V)) /\ b~=B}) : ReaderInfo})
	pre IsReader(R, (C,V)) /\ B isin GetReaderBooks (R, (C,V))

end