scheme abstract =
  class
    type 
      Supplier,
      Place,
      Name,
      Volume = Int, /* needs to be defined for getLowXXX functions */

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

      ItemInfo,
      DB

    value
      empty: DB,
      isPlaceFree: DB >< Place -> Bool,
      makeItem: Name >< Volume >< Supplier -> ItemInfo,
      getName: ItemInfo -> Name,
      getVolume: ItemInfo -> Volume,
      getSupplier: ItemInfo -> Supplier,
      addItem: DB >< Place >< ItemInfo -~-> DB,
      removeItem: DB >< Place -~-> DB,
      getItem: DB >< Place -~-> ItemInfo,
      updateItemName: DB >< Place >< Name -~-> DB,
      updateItemVolume: DB >< Place >< Volume -~-> DB,
      updateItemSupplier: DB >< Place >< Supplier -~-> DB,
      getPlaces: DB -> Places,
      getNames: DB -> Items,
      getSuppliers: DB -> Suppliers,
      getItemSuppliers: DB >< Name -> Suppliers,
      getItemPlaces: DB >< Name -> Places,
      getLowPlaces: DB >< Volume -> Places,
      getLowNames: DB >< Volume -> Items,
      dummy: Bool

    axiom
      /* isPlaceFree */
      all place: Place :-
        isPlaceFree(empty, place) is true,
      all db: DB, place_inside, place: Place, info: ItemInfo :-
        isPlaceFree(addItem(db, place_inside, info), place) is
          if (place_inside = place) then
            false
          else
            isPlaceFree(db, place)
          end,

      all name: Name, volume: Volume, supplier: Supplier :-
        getName(makeItem(name, volume, supplier)) is name,
      all name: Name, volume: Volume, supplier: Supplier :-
        getVolume(makeItem(name, volume, supplier)) is volume,
      all name: Name, volume: Volume, supplier: Supplier :-
        getSupplier(makeItem(name, volume, supplier)) is supplier,

      /* addItem is any function that matches removeItem, getItem */
      /* removeItem */
      all db: DB, place_inside, place: Place, info: ItemInfo :-
        removeItem(addItem(db, place_inside, info), place) is
          if (place_inside = place) then
            db
          else
            addItem(removeItem(db, place), place_inside, info)
          end,
      /* getItem */
      all db: DB, place_inside, place: Place, info: ItemInfo :-
        getItem(addItem(db, place_inside, info), place) is
          if (place_inside = place) then
            info
          else
            getItem(db, place)
          end,

      /* updateItemName */
      all db: DB, place_inside, place: Place, name: Name, info: ItemInfo :-
        updateItemName(addItem(db, place_inside, info), place, name) is
          if (place_inside = place) then
            addItem(db, place, makeItem(name, getVolume(info), getSupplier(info)))
          else
            addItem(updateItemName(db, place, name), place_inside, info)
          end,  
      /* updateItemVolume */
      all db: DB, place_inside, place: Place, volume: Volume, info: ItemInfo :-
        updateItemVolume(addItem(db, place_inside, info), place, volume) is
          if (place_inside = place) then
            addItem(db, place, makeItem(getName(info), volume, getSupplier(info)))
          else
            addItem(updateItemVolume(db, place, volume), place_inside, info)
          end,
      /* updateItemSupplier */
      all db: DB, place_inside, place: Place, supplier: Supplier, info: ItemInfo :-
        updateItemSupplier(addItem(db, place_inside, info), place, supplier) is
          if (place_inside = place) then
            addItem(db, place, makeItem(getName(info), getVolume(info), supplier))
          else
            addItem(updateItemSupplier(db, place, supplier), place_inside, info)
          end,

      /* the following functions rely on set structure of results */
      /* getPlaces */
      getPlaces(empty) is {},
      all db: DB, place: Place, info: ItemInfo :-
        getPlaces(addItem(db, place, info)) is 
          getPlaces(db) union {place},
      /* getNames */
      getNames(empty) is {},
      all db: DB, place: Place, info: ItemInfo :-
        getNames(addItem(db, place, info)) is
          getNames(db) union {getName(info)},
      /* getSuppliers */
      getSuppliers(empty) is {},
      all db: DB, place: Place, info: ItemInfo :-
        getSuppliers(addItem(db, place, info)) is
          getSuppliers(db) union {getSupplier(info)},

      /* getItemSuppliers */
      all name: Name :-
        getItemSuppliers(empty, name) is {},
      all db: DB, place: Place, name: Name, info: ItemInfo :-
        getItemSuppliers(addItem(db, place, info), name) is
          if (getName(info) = name) then
            getItemSuppliers(db, name) union {getSupplier(info)}
          else
            getItemSuppliers(db, name)
          end,
      /* getItemPlaces */
      all name: Name :-
        getItemPlaces(empty, name) is {},
      all db: DB, place: Place, name: Name, info: ItemInfo :-
        getItemPlaces(addItem(db, place, info), name) is
          if (getName(info) = name) then
            getItemPlaces(db, name) union {place}
          else
            getItemPlaces(db, name)
          end,

      /* getLowPlaces */
      all volume: Volume :-
        getLowPlaces(empty, volume) is {},
      all db: DB, place: Place, volume: Volume, info: ItemInfo :-
        getLowPlaces(addItem(db, place, info), volume) is
          if (getVolume(info) <= volume) then
            getLowPlaces(db, volume) union {place}
          else
            getLowPlaces(db, volume)
          end,
      /* another version follows... */
      /*
      all db: DB, place: Place, volume: Volume, places: Places :-
        getLowPlaces(db, volume) = places /\
        (all p: Place :- p isin places =>
                         getVolume(getItem(db, p)) <= volume),
      */
      /* getLowNames */
      all volume: Volume :-
        getLowNames(empty, volume) is {},
      all db: DB, place: Place, volume: Volume, info: ItemInfo :-
        getLowNames(addItem(db, place, info), volume) is
          if (getVolume(info) <= volume) then
            getLowNames(db, volume) union {getName(info)}
          else
            getLowNames(db, volume)
          end,

      dummy is true
  end