How to represent unique attribute in Z-notation without quantifiers?

Question

Full disclosure, this is for a university course. I don't expect an answer outright, but help would be appreciated.

I need to model an Item entity using Z-notation. This is the description:

Item: Every item has a name and a unique ID which can be used to uniquely describe the item. An item also has a price (positive float) and a category.

Part of the requirement is modelling these entities without quantifiers.

This is what I ended up with, but I'm not sure that it's correct:

Schema for Item

The idea being that the name is some combination of strings, the ID is a tuple of a positive integer and said name, and both the price and the category are mapped with total functions.

The first predicate is to ensure a positive price, the second is to ensure the uniqueness of the ID, i.e. reduce the domain to all integers that are not already assigned. I don't think this is correct, though.

Answer 1

The main issue with your approach is that you try to put information about the whole system (or part of it) into the description of a single item. E.g. you specified the price as a mapping from the id to a float - which is fine in principle - but you do not have such a function for each item.

There are many ways to specify this, I show two approaches:

1. You have two schemas: E.g. Item and Database

   +-- Item -----
   | id: ℕ
   | name: String
   | price: ℝ
   | category: String
   |----
   | price ≥ 0
   +----------
   
   +-- Database -----
   | items: ℕ +-> Item
   |----------
   

   This way you have the ID of each item moved from the item itself. When each item has also a field id, it would be complicated to state without quantifiers the fact that items should map an id to an item with the same id. Or when you just use a set of items it would be complicated to describe without quantifiers that two items must have distinct identifiers.

The uniqueness of the id for each item is guaranteed by items being a function.

2. Or just use several functions for each aspect of an item:

   +-- Items -----
   | ids: ℕ
   | name: ids --> String
   | price: ids --> ℝ
   | category: ids --> String
   +----------
   

   But stating the fact that all prices must be non-negative without quantifiers would be hard. Maybe by replacing ℝ by { x:ℝ | x≥0}.

A general remark: Do you need compute with your IDs? Maybe you can introduce a type with [ID] instead. The same applies for the category (e.g. [CATEGORY]).

And is the name not just a single string? But I don't think it would be a set of (unordered) strings.