scheme test=
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)),

/*==============================================================*/

	message: Text -> Unit
	message(t) is (),

	IsBookDriver : Book >< Library -> Bool
	IsBookDriver (B,(C,V)) is
	if let f=IsBook(B,(C,V)) in
		if f then (exists (B,a,q) : BookInfo :- (B,a,q) isin C)
		else (all (B,a,q) : BookInfo :- (B,a,q) ~isin C)
		end end then true
	else
		local in message ("IsInit"); false end
	end,

	GetAvailableDriver : Book >< Library -> Bool
	GetAvailableDriver (B,(C,V)) is
	if ~IsBook(B,(C,V)) then
		local in message("GetAvailable"); false end
	else
		if let s=GetAvailable(B,(C,V)) in
			(exists (b,a,q): BookInfo :- (b,a,q) isin C /\ b=B /\ a=s)
		end then true
		else local in message("GetAvailable"); false end
		end
	end,

	GetQTYDriver : Book >< Library -> Bool
	GetQTYDriver (B,(C,V)) is
	if ~IsBook(B,(C,V)) then
		local in message("precondition GetQTY"); false end
	else
		if let s=GetQTY(B,(C,V)) in
			(exists (b,a,q): BookInfo :- (b,a,q) isin C /\ b=B /\ q=s)
		end then true
		else local in message("GetQTY"); false end
		end
	end,

	IsReaderDriver : Reader >< Library -> Bool
	IsReaderDriver (R,(C,V)) is
	if let f=IsReader(R,(C,V)) in
		if f then (exists (r,bs) : ReaderInfo :- (r,bs) isin V /\ r=R)
		else (all (r,bs) : ReaderInfo :- (r,bs) ~isin V /\ r=R)
		end end then true
	else
		local in message("IsReader"); false end
	end,
		
	HaveABookDriver: Book >< Reader >< Library -> Bool
	HaveABookDriver (B,R,(C,V)) is
	if ~(IsReader(R,(C,V)) /\ IsBook(B,(C,V))) then
		local in message("precondition HaveABook"); false end
	else
		if let f=HaveABook(B,R,(C,V)) in
			if f then (exists (r,bl):ReaderInfo :- r=R /\ B isin bl /\ (r,bl) isin V)
			else (all (r,bl):ReaderInfo :- r=R /\ B ~isin bl /\ (r,bl) isin V)
			end end then true
		else local in message("HaveABook"); false end
		end
	end,

	BookInfoByBookDriver: Book >< Library -> Bool
	BookInfoByBookDriver (B,(C,V)) is
	if ~IsBook(B,(C,V)) then
		local in message("precondition BookInfoByBook"); false end
	else
		if let c=BookInfoByBook(B,(C,V)) in
		(exists (B,a,q): BookInfo :- (B,a,q) isin c /\ a=GetAvailable(B,(C,V)) /\ q=GetQTY(B,(C,V)))
		end then true
		else local in message("BookInfoByBook"); false end
		end
	end,

	ReaderInfoByReaderDriver: Reader >< Library -> Bool
	ReaderInfoByReaderDriver (R,(C,V)) is
	if ~IsReader (R,(C,V)) then
		local in message("precondition ReadeInfoByReader"); false end
	else
		if let v=ReaderInfoByReader(R,(C,V)) in
		(exists (R,bl): ReaderInfo :- (R,bl) isin v /\ (R,bl) isin V /\ bl=GetReaderBooks(R,(C,V)))
		end then true
		else local in message("ReaderInfoByReader"); false end
		end
	end,

	AddBookDriver : Book >< Library >< Nat-> Bool
	AddBookDriver (B,(C,V),c) is
	if GetQTY( B,(C,V)) > 0 then
		if let (cc,vv)=AddBook(B,(C,V),c) in
		(all (b,a,q):BookInfo :- cc<<=C /\ vv<<=V /\ (b,a,q) isin C /\ a=GetAvailable(B,(C,V))+c /\ q=GetQTY(B,(C,V))+c)
		end then true
		else local in message("AddBook"); false end
		end
	else
		if let (cc,vv)=AddBook(B,(C,V),c) in
		(all (b,a,q):BookInfo :- cc<<=C /\ vv<<=V /\ (b,a,q) isin C /\ a=c /\ q=c)
		end then true
		else local in message("AddBook"); false end
		end
	end,

	DeleteBookDriver : Book >< Library >< Nat -> Bool
	DeleteBookDriver(B,(C,V),c) is
	if ~(GetQTY(B,(C,V)) >0 /\ c>0) then
		local in message("DeleteBook"); false end
	else
		if c < GetAvailable (B,(C,V)) then
			if let (cc,vv)=DeleteBook(B,(C,V),c) in
			(all (b,a,q):BookInfo :- cc<<=C /\ vv<<=V /\ (b,a,q) isin C /\ a=GetAvailable(B,(C,V))-c /\ q=GetQTY(B,(C,V))-c)
			end then true
			else local in message("DeleteBook"); false end
			end
		else
			if let (cc,vv)=DeleteBook(B,(C,V),c) in
			(all (b,a,q):BookInfo :- cc<<=C /\ vv<<=V /\ (b,a,q) isin C /\ a=0 /\ q=GetQTY(B,(C,V))-GetAvailable(B,(C,V)))
			end then true
			else local in message("DeleteBook"); false end
			end
		end
	end,

	AddReaderDriver : Reader >< Library -> Bool
	AddReaderDriver (R,(C,V)) is 
	if IsReader(R,(C,V)) then
		local in message("precondition AddReader"); false end
	else
		if let (cc,vv)=AddReader(R,(C,V)) in
		(all (R,bl):ReaderInfo :- (R,bl) ~isin vv)
		end then true
		else local in message("AddReader"); false end
		end
	end,
	
	GetReaderBooksDriver : Reader >< Library -~-> Bool
	GetReaderBooksDriver (R,(C,V)) is
	if ~IsReader(R,(C,V)) then
		local in message("precondition GetReaderBooks"); false end
	else
		if let bl=GetReaderBooks(R,(C,V)) in
		(all b:Book:-HaveABook(b,R,(C,V)))
		end then true
		else local in message("GetReaderBooks"); false end
		end
	end,

	DeleteReaderDriver : Reader >< Library -> Bool
	DeleteReaderDriver (R,(C,V)) is
	if ~(IsReader (R,(C,V)) /\ GetReaderBooks(R,(C,V)) = {}) then
		local in message("precondition DeleteReader"); false end
	else
		if let l=DeleteReader(R,(C,V)) in
		(all (R,bl):ReaderInfo :- (R,bl) ~isin V)
		end then true
		else local in message("DeleteReader"); false end
		end
	end,

	GiveBookDriver: Book >< Reader >< Library -~-> Bool
	GiveBookDriver (B,R,(C,V)) is 
	if ~(GetAvailable (B, (C,V)) >0  /\ IsReader(R, (C,V)) /\ B ~isin GetReaderBooks (R, (C,V))) then
		local in message("precondition GiveBook"); false end
	else
		if let (cc,vv)=GiveBook(B,R,(C,V)) in
		(exists (R,bl):ReaderInfo :- (R,bl) isin vv /\ B isin bl /\ GetAvailable(B,(C,V))=GetAvailable(B,(C,vv))+1)
		end then true
		else local in message("GiveBook"); false end
		end
	end,

	ReturnBookDriver: Book >< Reader >< Library -~-> Bool
	ReturnBookDriver (B,R,(C,V)) is 
	if ~(IsReader(R, (C,V)) /\ B isin GetReaderBooks (R, (C,V))) then
		local in message("precondition ReturnBook"); false end
	else
		if let (cc,vv)=GiveBook(B,R,(C,V)) in
		(all (R,bl):ReaderInfo :- (R,bl) isin vv /\ B ~isin bl /\ GetAvailable(B,(C,V))=GetAvailable(B,(C,vv))-1)
		end then true
		else local in message("ReturnBook"); false end
		end
	end

end