scheme testing =
  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) is place ~isin dom(db),

      getName: ItemInfo -> Name
        getName((name, volume, supplier)) is name,
      getVolume: ItemInfo -> Volume
        getVolume((name, volume, supplier)) is volume,
      getSupplier: ItemInfo -> Supplier
        getSupplier((name, volume, supplier)) is supplier,

      addItem: DB >< Place >< ItemInfo -~-> DB
        addItem(db, place, info) is db union [place +> info]
        pre isPlaceFree(db, place),
      removeItem: DB >< Place -~-> DB
        removeItem(db, place) is db \ {place}
        pre ~isPlaceFree(db, place),
      getItem: DB >< Place -~-> ItemInfo
        getItem(db, place) is db(place)
        pre ~isPlaceFree(db, place),

      updateItemName: DB >< Place >< Name -~-> DB
        updateItemName(db, place, name_new) is
          let (name, volume, supplier) = db(place) in
            addItem(removeItem(db, place), place, (name_new, volume, supplier))
          end
        pre ~isPlaceFree(db, place),
      updateItemVolume: DB >< Place >< Volume -~-> DB
        updateItemVolume(db, place, volume_new) is
          let (name, volume, supplier) = db(place) in
            addItem(removeItem(db, place), place, (name, volume_new, supplier))
          end
        pre ~isPlaceFree(db, place),
      updateItemSupplier: DB >< Place >< Supplier -~-> DB
        updateItemSupplier(db, place, supplier_new) is
          let (name, volume, supplier) = db(place) in
            addItem(removeItem(db, place), place, (name, volume, supplier_new))
          end
        pre ~isPlaceFree(db, place),

      getPlaces: DB -> Places
        getPlaces(db) is dom(db),
      getNames: DB -> Items
        getNames(db) is
          { n | n: Name :- (
            exists p: Place :- n = getName(getItem(db, p))
          ) },
      getSuppliers: DB -> Suppliers
        getSuppliers(db) is
          { s | s: Supplier :- (
            exists p: Place :- s = getSupplier(getItem(db, p))
          ) },
      getItemSuppliers: DB >< Name -> Suppliers
        getItemSuppliers(db, name_search) is
          { s | s: Supplier :- (
            exists p: Place :- (name_search = getName(getItem(db, p))) /\
                               (s = getSupplier(getItem(db, p)))
          ) },
      getItemPlaces: DB >< Name -> Places
        getItemPlaces(db, name_search) is
          { p | p: Place :- name_search = getName(getItem(db, p)) },

      getLowPlaces: DB >< Volume -> Places
        getLowPlaces(db, volume_low) is
          { p | p: Place :- let (name, volume, supplier) = getItem(db, p) in
            volume <= volume_low
          end },
      getLowNames: DB >< Volume -> Items
        getLowNames(db, volume_low) is
          { n | n: Name :- (exists p: Place :-
            let (n, volume, supplier) = getItem(db, p) in
              volume <= volume_low
            end
          ) },



      Trass : Text -> Unit
        Trass(T) is (),  

      isPlaceFreeDriver: DB >< Place -> Bool
        isPlaceFreeDriver(db, place) is
          if isPlaceFree(db, place) = ~(place isin dom(db)) then
            true
          else
            local in Trass("isPlaceFree"); false end
          end,

      getNameDriver: ItemInfo -> Bool
        getNameDriver((name, volume, supplier)) is
          if getName((name, volume, supplier)) = name then
            true
          else
            local in Trass("getName"); false end
          end,

      getVolumeDriver: ItemInfo -> Bool
        getVolumeDriver((name, volume, supplier)) is
          if getVolume((name, volume, supplier)) = volume then
            true
          else
            local in Trass("getVolume"); false end
          end,
	
      getSupplierDriver: ItemInfo -> Bool
        getSupplierDriver((name, volume, supplier)) is
          if getSupplier((name, volume, supplier)) = supplier then
            true
          else
            local in Trass("getVolume"); false end
          end,

      addItemDriver: DB >< Place >< ItemInfo -> Bool
        addItemDriver(db, place, info) is
          if ~isPlaceFree(db, place) then
            local in Trass("precondition addItem"); false end
          else
          if let res = addItem(db, place, info) in
            (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) end then
            true
          else
            local in Trass("addItem"); false end
          end
          end,

      removeItemDriver: DB >< Place -> Bool
        removeItemDriver(db, place) is
          if isPlaceFree(db, place) then
            local in Trass("precondition removeItem"); false end
          else
          if let res = removeItem(db, place) in
	    (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)) end then
            true
          else
            local in Trass("removeItem"); false end
          end
          end,

      getItemDriver: DB >< Place -> Bool
        getItemDriver(db, place) is
          if isPlaceFree(db, place) then
            local in Trass("precondition getItem"); false end
          else
          if let res = getItem(db, place) in
            db(place) = res end then
            true
          else
            local in Trass("getItem"); false end
          end
          end,

      updateItemNameDriver: DB >< Place >< Name -> Bool
        updateItemNameDriver(db, place, name_new) is
          if isPlaceFree(db, place) then
            local in Trass("precondition updateItemName"); false end
          else
          if let res = updateItemName(db, place, name_new) in
	    (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))) end then
            true
          else
            local in Trass("updateItemName"); false end
          end
          end,


	
      updateItemVolumeDriver: DB >< Place >< Volume -> Bool
        updateItemVolumeDriver(db, place, volume_new) is
          if isPlaceFree(db, place) then
            local in Trass("precondition updateItemVolume"); false end
          else
          if let res = updateItemVolume(db, place, volume_new) in
  	    (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))) end then
            true
          else
            local in Trass("updateItemVolume"); false end
          end
          end,
	
      updateItemSupplierDriver: DB >< Place >< Supplier -> Bool
        updateItemSupplierDriver(db, place, supplier_new) is
          if isPlaceFree(db, place) then
            local in Trass("precondition updateItemSupplier"); false end
          else
          if let res = updateItemSupplier(db, place, supplier_new) in
	    (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) end then
            true
          else
            local in Trass("updateItemSupplier"); false end
          end
          end,

      getPlacesDriver: DB -> Bool
        getPlacesDriver(db) is
          if let res = getPlaces(db) in
            dom(db) = res end then
            true
          else
            local in Trass("getPlaces"); false end
          end,
    
      getNamesDriver: DB -> Bool
        getNamesDriver(db) is
          if let res = getNames(db) in
	    (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)) end then
            true
          else
            local in Trass("getNames"); false end
          end,

      getSuppliersDriver: DB -> Bool
        getSuppliersDriver(db) is
          if let res = getSuppliers(db) in
	    (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)) end then
            true
          else
            local in Trass("getSuppliers"); false end
          end,
	    
      getItemSuppliersDriver: DB >< Name -> Bool
        getItemSuppliersDriver(db, name_search) is
          if let res = getItemSuppliers(db, name_search) in
	    (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)) end then
            true
          else
            local in Trass("getItemSuppliers"); false end
          end,
	      
      getItemPlacesDriver: DB >< Name -> Bool
        getItemPlacesDriver(db, name_search) is
          if let res = getItemPlaces(db, name_search) in
	    (all pl: Place :- getName(db(pl)) = name_search =>
	      pl isin res) /\
	    (all pl: Place :- pl isin res =>
	      getName(db(pl)) = name_search) end then
            true
          else
            local in Trass("getItemPlaces"); false end
          end,

      getLowPlacesDriver: DB >< Volume -> Bool
        getLowPlacesDriver(db, volume_low) is
          if let res = getLowPlaces(db, volume_low) in
	    (all pl: Place :- getVolume(db(pl)) <= volume_low =>
	      pl isin res) /\
	    (all pl: Place :- pl isin res =>
	      getVolume(db(pl)) <= volume_low) end then
            true
          else
            local in Trass("getLowPlaces"); false end
          end,

      getLowNamesDriver: DB >< Volume -> Bool
        getLowNamesDriver(db, volume_low) is
          if let res = getLowNames(db, volume_low) in
	    (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))) end then
            true
          else
            local in Trass("getLowPlaces"); false end
          end,

      dummy: Bool = true
  end