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

      dummy: Bool = true
  end