scheme test =
	class
	type
		ProdName=Text,
		CompName=Text,
		Product=ProdName >< CompName,
		Place=Nat,
		QTY=Nat,
		ProdInfo=Product >< QTY >< Place,
		Stock=ProdInfo-set
	value

		allNaturalNumbers: Nat-inflist
	axiom
		allNaturalNumbers(1)=0,
		all idx: Nat :- idx>=2 => allNaturalNumbers(idx)=allNaturalNumbers(idx-1)+1
	value



		construct: Product >< Stock -~-> Stock
		construct(Prod,St) is
			St union {(Prod,0,0)}
			pre ~ isInit(Prod,St),



		destruct: Product >< Stock -~-> Stock
		destruct(Prod,St) is
			{(p,c,d) | (p,c,d): ProdInfo :- (p,c,d) isin St /\ p~=Prod}
			pre isInit(Prod,St),



		isInit: Product >< Stock -> Bool
		isInit(P,St) is
			(exists (Prod,k,l): ProdInfo :- (Prod,k,l) isin St /\ P=Prod),



		forProduct: Product >< Stock -> Stock
		forProduct(P,St) is
			{(prod,k,l) | (prod,k,l):ProdInfo :- (prod,k,l) isin St /\ prod=P},



		forPlace: Place >< Stock -> Stock
		forPlace(Pl,St) is
			{((i,j),k,l) | ((i,j),k,l):ProdInfo :- ((i,j),k,l) isin St /\ l=Pl},



		needOfProduct: QTY >< Stock -> Product-set
		needOfProduct(A,St) is
			{Prod | Prod:Product :- qtyOfProduct(Prod,St)<=A},



		Stock_to_list: Stock -~-> QTY-list
		Stock_to_list(St) is
			<.n | n in allNaturalNumbers :- all (Prod,k,l):ProdInfo :- (Prod,k,l) isin St /\ n=k.>
			pre St~={},



		summ_elems_of_list: QTY-list -> QTY
		summ_elems_of_list(list) is
			if (list=<..>) then 0
				else hd list + summ_elems_of_list(tl list)
			end,



		qtyOfProduct: Product >< Stock -~-> QTY
		qtyOfProduct(Prod,St) is
			summ_elems_of_list(Stock_to_list(forProduct(Prod,St)))
			pre isInit(Prod,St),



		setAllProdName: Stock -~-> ProdName-set
		setAllProdName(St) is
			{i | i:ProdName :- all ((i,j),k,l):ProdInfo :- ((i,j),k,l) isin St /\ k>0}
			pre St~={},



		IsGreat: ProdInfo >< Stock -~-> QTY
		IsGreat((P,k,l),St) is
			if (exists (P,c,l):ProdInfo :- (P,c,l) isin St /\ c>=k) then qtyhelp((P,k,l),St)(1)
				else 0
			end
			pre isInit(P,forPlace(l,St)),



		qtyhelp: ProdInfo >< Stock -> QTY-list
		qtyhelp((P,k,l),St) is
			<.q | q in Stock_to_list(forPlace(l,forProduct(P,St))) :- q>=k.>,


		
		addToStock: ProdInfo >< Stock -~-> Stock
		addToStock((P,k,l),St) is
			if (isInit(P,forPlace(l,St))) then St\{(P,qk,l) | (P,qk,l): ProdInfo :- qk=IsGreat((P,0,l),St)} union {(P,newqty,l) | (P,newqty,l):ProdInfo :- newqty=k+IsGreat((P,0,l),St)}
				else St union {(P,k,l)}
			end
			pre isInit(P,St) /\ k>0 /\ l>0,



		deleteFromPlace: ProdInfo >< Stock -~-> Stock
		deleteFromPlace((Prod,k,l),St) is
			if (k<IsGreat((Prod,k,l),St)) then St\{(Prod,c,l) | (Prod,c,l): ProdInfo :- c=IsGreat((Prod,0,l),St)} union {(Prod,newqty,l) | (Prod,newqty,l):ProdInfo :- newqty=IsGreat((Prod,k,l),St)-k}
				else St\{(Prod,k,l)} union {(Prod,0,0)}
			end
			pre k<=IsGreat((Prod,k,l),St) /\ k>0 /\ l>0,



		changeOfProduct: ProdInfo >< Place >< Stock -~-> Stock
		changeOfProduct((Prod,k,l),PL,St) is
			if (IsGreat((Prod,0,PL),St)>=0) then deleteFromPlace((Prod,k,l),St) union addToStock((Prod,k,PL),St)
				else deleteFromPlace((Prod,k,l),St) union {(Prod,k,PL)}
			end
			pre IsGreat((Prod,0,l),St)>=k /\ k>0 /\ PL>0,



		listOFPlaces: Product >< Stock -> Place-list
		listOFPlaces(P,St) is
			<.n | n in allNaturalNumbers :- all (P,y,z): ProdInfo :- (P,y,z) isin St /\ n=z.>,



		placeQTY: Product >< Stock -> QTY-list
		placeQTY(P,St) is
			<.n | n in allNaturalNumbers :- all (P,y,z): ProdInfo :- (P,y,z) isin St /\ z= hd listOFPlaces(P,St) /\ n=y.>,



		deleteFromStock: Product >< QTY >< Stock -~-> Stock
		deleteFromStock(P,QT,St) is
			if (exists (P,y,z): ProdInfo :- (P,y,z) isin St /\ z=hd listOFPlaces(P,St) /\ y>QT) then St\{(P,n,m) | (P,n,m): ProdInfo :- (P,n,m) isin St /\ m=hd listOFPlaces(P,St)} union {(P,hd placeQTY(P,St)-QT,hd listOFPlaces(P,St))}
				elsif (exists (P,QT,z):ProdInfo :- (P,QT,z) isin St /\ z=hd listOFPlaces(P,St)) then if (exists (P,y,z): ProdInfo :- (P,y,z) isin St /\ z~=hd listOFPlaces(P,St)) then St\{(P,QT,z) | (P,QT,z): ProdInfo :- z=hd listOFPlaces(P,St)}
					else St\{(P,QT,z) | (P,QT,z): ProdInfo :- z=hd listOFPlaces(P,St)} union {(P,0,0)}
				end
			else deleteFromStock(P,QT-hd placeQTY(P,St),St\{(P,x,y) | (P,x,y): ProdInfo :- (P,x,y) isin St /\ x=hd placeQTY(P,St) /\ y=hd listOFPlaces(P,St)})
			end
			pre qtyOfProduct(P,St)>=QT,



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

		constructDriver: Product >< Stock -> Bool
		constructDriver(Prod,St) is
			if isInit(Prod,St) then
				local in message("precondition construct"); false end
			else
				if let S=construct(Prod,St) in isInit(Prod,S) /\ S>>St end
					then true
				else 
					local in message("construct"); false end
				end
			end,

		destructDriver: Product >< Stock -> Bool
		destructDriver(Prod,St) is
			if ~isInit(Prod,St) then
				local in message ("precondition destruct"); false end
			else
				if let S=destruct(Prod,St) in ~isInit(Prod,S) /\ S<<St end
					then true
				else
					local in message("destruct"); false end
				end
			end,

		isInitDriver: Product >< Stock -> Bool
		isInitDriver(P,St) is
			if let b=isInit(P,St) in 
				if b then (exists (Pr,x,y): ProdInfo :- (Pr,x,y) isin St)
					else (all (Pr,i,j): ProdInfo :- (Pr,i,j) ~isin St)
				end end then true
			else
				local in message("isInit"); false end
			end,
				
		forProductDriver: Product >< Stock -> Bool
		forProductDriver(P,St) is
			if let S=forProduct(P,St) in
				(all (P,k,l): ProdInfo :- S<<=St /\ (P,k,l) isin S) end
				then true
			else
				local in message("forProduct"); false end
			end,

		forPlaceDriver: Place >< Stock -> Bool
		forPlaceDriver(Pl,St) is
			if let S=forPlace(Pl,St) in
				(all ((i,j),k,Pl): ProdInfo :- ((i,j),k,Pl) isin S /\ S<<=St) end
				then true
			else
				local in message("forPlace"); false end
			end,

		needOfProductDriver: QTY >< Stock -> Bool
		needOfProductDriver(A,St) is
			if let Ps=needOfProduct(A,St) in
				(all Prod:Product :- qtyOfProduct(Prod,St)<=A /\ Prod isin Ps) end
				then true
			else
				local in message("needOfProduct"); false end
			end,

		qtyOfProductDriver: Product >< Stock -> Bool
		qtyOfProductDriver(Prod,St) is
			if ~isInit(Prod,St) then
				local in message("precondition qtyOfProduct"); false end
			else
				if let summa=qtyOfProduct(Prod,St) in
					(exists (Prod,QT,Pl): ProdInfo :- (Prod,QT,Pl) isin St /\ summa >=QT) end
					then true
				else
					local in message("qtyOfProduct"); false end
				end
			end,

		setAllProdNameDriver: Stock -> Bool
		setAllProdNameDriver(St) is
			if St={} then
				local in message("precondition setAllProdName"); false end
			else
				if let S=setAllProdName(St) in
					(all ((i,j),k,l):ProdInfo :- ((i,j),k,l) isin St /\ k>0 /\ i isin S) end
					then true
				else
					local in message("setAllProdName"); false end
				end
			end,

		addToStockDriver: Product >< QTY >< Place >< Stock -> Bool
		addToStockDriver(P,QT,Pl,St) is
			if ~(isInit(P,St) /\ QT>0 /\ Pl>0) then
				local in message("precondition addToStock"); false end
			else
				if let ftp=addToStock((P,QT,Pl),St) in
					qtyOfProduct(P,forPlace(Pl,St))=qtyOfProduct(P,forPlace(Pl,ftp))-QT end
					then true
				else
					local in message("addToStock"); false end
				end
			end,

		changePlaceOfProductDriver: ProdInfo >< Place >< Stock -> Bool
		changePlaceOfProductDriver((P,QT,Pl1),Pl2,St) is
			if ~(qtyOfProduct(P,forPlace(Pl1,St))>=QT /\ QT>0 /\ Pl2>0) then
				local in message("precondition changeOfProduct"); false end
			else
				if let tty=changeOfProduct((P,QT,Pl1),Pl2,St) in
					qtyOfProduct(P,forPlace(Pl2,tty))=qtyOfProduct(P,forPlace(Pl2,St))+QT /\ qtyOfProduct(P,forPlace(Pl1,tty))=qtyOfProduct(P,forPlace(Pl1,St))-QT end
					then true
				else
					local in message("changePlaceOfProduct"); false end
				end
			end,

		deleteFromStockDriver: Product >< QTY >< Stock -> Bool
		deleteFromStockDriver(P,QT,St) is
			if ~(qtyOfProduct(P,St)>=QT) then
				local in message("precondition deleteFromStock"); false end
			else
				if let www=deleteFromStock(P,QT,St) in
					qtyOfProduct(P,www)=qtyOfProduct(P,St)-QT /\ isInit(P,www) end
					then true
				else
					local in message("deleteFromStock"); false end
				end
			end,

		Stock_to_listDriver: Stock -> Bool
		Stock_to_listDriver(St) is
			if St={} then
				local in message("precondition Stock_to_list"); false end
			else
				if let yoyo=Stock_to_list(St) in
					(all (Prod,k,l):ProdInfo :- (Prod,k,l) isin St /\ k isin elems yoyo) end
					then true
				else
					local in message("Stock_to_list"); false end
				end
			end,

		summ_elems_of_listDriver: QTY-list -> Bool
		summ_elems_of_listDriver(list) is
			if let tt=summ_elems_of_list(list) in
				tt>=hd list end
				then true
			else
				local in message("summ_elems_of_list"); false end
			end,

		IsGreatDriver: ProdInfo >< Stock -> Bool
		IsGreatDriver((P,k,l),St) is
			if ~(isInit(P,forPlace(l,St))) then
				local in message("precondition IsGreat"); false end
			else
				if let br=IsGreat((P,k,l),St) in
					br>=0 end
					then true
				else
					local in message("IsGreat"); false end
				end
			end,


		qtyhelpDriver: ProdInfo >< Stock -> Bool
		qtyhelpDriver((P,k,l),St) is
			if let hr=qtyhelp((P,k,l),St) in
				elems hr <<= elems Stock_to_list(forPlace(l,forProduct(P,St))) end
				then true
			else
				local in message("qtyhelp"); false end
			end,

		listOFPlacesDriver: Product >< Stock -> Bool
		listOFPlacesDriver(P,St) is
			if let cow=listOFPlaces(P,St) in
				(all (P,y,z): ProdInfo :- (P,y,z) isin St /\ z isin elems cow) end
				then true
			else
				local in message("listOFPlaces"); false end
			end,
                            
		placeQTYDriver: Product >< Stock -> Bool
		placeQTYDriver(P,St) is
			if let cover=placeQTY(P,St) in
				(all (P,y,z): ProdInfo :- (P,y,z) isin St /\ z= hd listOFPlaces(P,St) /\ y isin elems cover) end
				then true
			else
				local in message("placeQTY"); false end
			end

	end