scheme implicit =
	class
	type
		ProdName=Text,			/*Наименование товара*/
		CompName=Text,			/*Наименование производителя*/
		Product=ProdName >< CompName,	/*Конкретный товар*/
		Place=Nat,			/*Местоположение товара*/
		QTY=Nat,			/*Количество товара*/
		ProdInfo=Product >< QTY >< Place,/*Информация о конкретном товаре*/
		Stock=ProdInfo-set		/*Склад товаров*/
	value

	/*Инициализация продукта*/

		construct: Product >< Stock -~-> Stock
		construct(Prod,St) as S
			post IsInit(Prod,S) /\ S>>St
			pre ~ IsInit(Prod,St),

	/*Деинициализация продукта*/

		destruct: Product >< Stock -~-> Stock
		destruct(Prod,St) as S
			post ~IsInit(Prod,S) /\ S<<St
			pre IsInit(Prod,St),

	/*Проверка наличия информации о конкретном товаре на складе*/

		IsInit: Product >< Stock -> Bool
		IsInit(P,St) as b
			post if b then (exists (P,x,y): ProdInfo :- (P,x,y) isin St)
				else (all (P,i,j): ProdInfo :- (P,i,j) ~isin St)
				end,

	/*Выдача информации по конкретному товару*/

		forProduct: Product >< Stock -> Stock
		forProduct(P,St) as S
			post (all (P,k,l): ProdInfo :- S<<=St /\ (P,k,l) isin S),

	/*Выдача информации по конкретной полке*/

		forPlace: Place >< Stock -> Stock
		forPlace(Pl,St) as S
			post (all ((i,j),k,Pl): ProdInfo :- ((i,j),k,Pl) isin S /\ S<<=St),

	/*Выдача конкретных товаров, нуждающихся в дозакупке*/

		needofProduct: QTY >< Stock -> Product-set
		needofProduct(A,St) as Ps
			post (all Prod:Product :- qtyofProduct(Prod,St)<=A /\ Prod isin Ps),

	/*Вспомогательная функция, формирующая из множества товаров список их количеств*/

		Stock_to_list: Stock -~-> QTY-list
		Stock_to_list(St) as yoyo
			post (all (Prod,k,l):ProdInfo :- (Prod,k,l) isin St /\ k isin elems yoyo)
			pre St~={},

	/*Вспомогательная функция, выдающая сумму всех элементов списка*/

		summ_elems_of_list: QTY-list -> QTY
		summ_elems_of_list(list) as tt
			post tt>=hd list,

	/*Подсчёт количества конкретного товара*/

		qtyofProduct: Product >< Stock -~-> QTY
		qtyofProduct(Prod,St) as summa
			post (exists (Prod,QT,Pl): ProdInfo :- (Prod,QT,Pl) isin St /\ summa >=QT)
			pre IsInit(Prod,St),


	/*Множество всех наименований товаров, присутствующих на складе*/

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

	/*Добавление данного количества конкретного продукта на склад*/
		
		addToStock: Product >< QTY >< Place >< Stock -~-> Stock
		addToStock(P,QT,Pl,St) as ftp
			post qtyofProduct(P,forPlace(Pl,St))=qtyofProduct(P,forPlace(Pl,ftp))-QT
			pre IsInit(P,St) /\ QT>0 /\ Pl>0,

	/*Изменение местоположения данного количества конкретного товара на складе*/

		changePlaceofProduct: ProdInfo >< Place >< Stock -~-> Stock
		changePlaceofProduct((P,QT,Pl1),Pl2,St) as tty
			post qtyofProduct(P,forPlace(Pl2,tty))=qtyofProduct(P,forPlace(Pl2,St))+QT /\ qtyofProduct(P,forPlace(Pl1,tty))=qtyofProduct(P,forPlace(Pl1,St))-QT
			pre qtyofProduct(P,forPlace(Pl1,St))>=QT /\ QT>0 /\ Pl2>0,

	/*Продажа конкретного продукта*/

		deleteFromStock: Product >< QTY >< Stock -~-> Stock
		deleteFromStock(P,QT,St) as www
			post qtyofProduct(P,www)=qtyofProduct(P,St)-QT /\ IsInit(P,www)
			pre qtyofProduct(P,St)>=QT

	end