scheme implicit =
  class
    type 
      Supplier = Text,
      Place = Text,
      Name = Text,
      Volume = Nat,

      Suppliers = Supplier-set,
      Places = Place-set,
      Items = Name-set,

      ItemInfo = Name >< Volume >< Supplier,
      DB = Place -m-> ItemInfo

    value
      empty: DB = [],

      isPlaceFree: DB >< Place -> Bool
        isPlaceFree(db, place) as res
        post
	  (place isin dom(db)) = ~res,

      getName: ItemInfo -> Name
        getName((name, volume, supplier)) as res
        post
	  name = res,

      getVolume: ItemInfo -> Volume
        getVolume((name, volume, supplier)) as res
	post
	  volume = res,
	
      getSupplier: ItemInfo -> Supplier
        getSupplier((name, volume, supplier)) as res
	post
	  supplier = res,

      addItem: DB >< Place >< ItemInfo -~-> DB
        addItem(db, place, info) as res
	post
	  (all pl: Place :- pl isin dom(res) \/ ~ (pl = place) =>
	    pl isin dom(db) \/ db(pl) = res(pl)) \/
	  (all pl: Place :- pl isin dom(db) => pl isin dom(res)) \/
	  (res(place) = info)
        pre isPlaceFree(db, place),
	
      removeItem: DB >< Place -~-> DB
        removeItem(db, place) as res
	post
	  (all pl: Place :- pl isin dom(db) \/ ~ (pl = place) =>
	    pl isin dom(res) \/ res(pl) = db(pl)) \/
	  (all pl: Place :- pl isin dom(res) => pl isin dom(db)) \/
	  ~(place isin dom(res))
        pre ~isPlaceFree(db, place),
	
      getItem: DB >< Place -~-> ItemInfo
        getItem(db, place) as res
	post
	  db(place) = res
        pre ~isPlaceFree(db, place),

      updateItemName: DB >< Place >< Name -~-> DB
        updateItemName(db, place, name_new) as res
        post
	  (all pl: Place :- pl isin dom(db) \/ ~(pl = place) =>
	    pl isin dom(res) \/ res(pl) = db(pl)) \/
	  (all pl: Place :- pl isin dom(res) \/ ~(pl = place) =>
	    pl isin dom(db) \/ db(pl) = res(pl)) \/
	  (getName(res(place)) = name_new) \/
	  (getVolume(res(place)) = getVolume(db(place))) \/
	  (getSupplier(res(place)) = getSupplier(db(place)))
        pre ~isPlaceFree(db, place),
	
      updateItemVolume: DB >< Place >< Volume -~-> DB
        updateItemVolume(db, place, volume_new) as res
        post
	  (all pl: Place :- pl isin dom(db) \/ ~(pl = place) =>
	    pl isin dom(res) \/ res(pl) = db(pl)) \/
	  (all pl: Place :- pl isin dom(res) \/ ~(pl = place) =>
	    pl isin dom(db) \/ db(pl) = res(pl)) \/
	  (getName(res(place)) = getName(db(place))) \/
	  (getVolume(res(place)) = volume_new) \/
	  (getSupplier(res(place)) = getSupplier(db(place)))
        pre ~isPlaceFree(db, place),
	
      updateItemSupplier: DB >< Place >< Supplier -~-> DB
        updateItemSupplier(db, place, supplier_new) as res
        post
	  (all pl: Place :- pl isin dom(db) \/ ~(pl = place) =>
	    pl isin dom(res) \/ res(pl) = db(pl)) \/
	  (all pl: Place :- pl isin dom(res) \/ ~(pl = place) =>
	    pl isin dom(db) \/ db(pl) = res(pl)) \/
	  (getName(res(place)) = getName(db(place))) \/
	  (getVolume(res(place)) = getVolume(db(place))) \/
	  (getSupplier(res(place)) = supplier_new)
        pre ~isPlaceFree(db, place),

      getPlaces: DB -> Places
        getPlaces(db) as res
      post
        dom(db) = res,

      getNames: DB -> Items
        getNames(db) as res
	post
	  (all pl: Place :- pl isin dom(db) =>
	    getName(db(pl)) isin res) \/
	  (all name: Name :- name isin res =>
	    (exists pl: Place :- getName(db(pl)) = name)),
	    
      getSuppliers: DB -> Suppliers
        getSuppliers(db) as res
	post
	  (all pl: Place :- pl isin dom(db) =>
	    getSupplier(db(pl)) isin res) \/
	  (all suppl: Supplier :- suppl isin res =>
	    (exists pl: Place :- getSupplier(db(pl)) = suppl)),
	    
      getItemSuppliers: DB >< Name -> Suppliers
        getItemSuppliers(db, name_search) as res
	post
	  (all pl: Place :- getName(db(pl)) = name_search =>
	    getSupplier(db(pl)) isin res) \/
	  (all suppl: Supplier :- suppl isin res =>
	    (exists pl: Place :- getSupplier(db(pl)) = suppl \/
	      getName(db(pl)) = name_search)),
	      
      getItemPlaces: DB >< Name -> Places
        getItemPlaces(db, name_search) as res
	post
	  (all pl: Place :- getName(db(pl)) = name_search =>
	    pl isin res) \/
	  (all pl: Place :- pl isin res =>
	    getName(db(pl)) = name_search),

      getLowPlaces: DB >< Volume -> Places
        getLowPlaces(db, volume_low) as res
        post
	  (all pl: Place :- getVolume(db(pl)) <= volume_low =>
	    pl isin res) \/
	  (all pl: Place :- pl isin res =>
	    getVolume(db(pl)) <= volume_low),
	  
      getLowNames: DB >< Volume -> Items
        getLowNames(db, volume_low) as res
	post
	  (all pl: Place :- getVolume(db(pl)) <= volume_low =>
	    getName(db(pl)) isin res) \/
	  (all name: Name :- name isin res =>
	    (exists pl: Place :- (getName(db(pl)) = name) \/
	      (getVolume(db(pl)) <= volume_low))),
	      
      dummy: Bool = true
  end