Как представить уникальный атрибут в Z-нотации без квантификаторов?

Question

Полное раскрытие, это для университетского курса.Я не ожидаю прямого ответа, но помощь будет принята.

Мне нужно смоделировать объект Item, используя Z-нотацию.Это описание:

Предмет: У каждого предмета есть имя и уникальный идентификатор, который можно использовать для уникального описания предмета.У элемента также есть цена (положительное значение с плавающей точкой) и категория.

Часть требований заключается в моделировании этих сущностей без квантификаторов.

Это то, что яв конечном итоге, но я не уверен, что это правильно:

Схема для элемента

Идея состоит в том, что имя представляет собой некоторую комбинацию строк, идентификаторкортеж из положительного целого числа и указанного имени, и цена, и категория сопоставляются с общими функциями.

Первый предикат - это обеспечение положительной цены, второй - обеспечение уникальности идентификатора,т.е. уменьшить домен до всех целых чисел, которые еще не назначены. Хотя я не думаю, что это правильно.

Answer 1

Основная проблема вашего подхода заключается в том, что вы пытаетесь поместить информацию обо всей системе (или ее части) в описание одного элемента.Например, вы указали цену как отображение идентификатора на число с плавающей точкой - что в принципе нормально - но у вас нет такой функции для каждого элемента.

Есть много способов указать это, я покажу дваподходы:

1. У вас есть две схемы: например, Item и Database

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

   Таким образом, у вас есть идентификатор каждого элемента, перемещенный из самого элемента,Когда у каждого элемента также есть поле id, было бы сложно указать без квантификаторов тот факт, что items должен сопоставить идентификатор с элементом с таким же идентификатором.Или, когда вы просто используете набор элементов, было бы сложно описать без квантификаторов, что два элемента должны иметь различные идентификаторы.

Уникальность идентификатора для каждого элемента гарантируется items будучи функцией.

Или просто используйте несколько функций для каждого аспекта элемента:

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

Но заявить, что все цены должны быть неотрицательными без квантификаторов, было бы сложно.Может быть, заменив ℝ на { x:ℝ | x≥0}.

Общее замечание: Вам нужно вычислить свои идентификаторы?Может быть, вы можете ввести тип с [ID] вместо этого.То же самое относится и к категории (например, [CATEGORY]).

И имя не просто строка?Но я не думаю, что это будет набор (неупорядоченных) строк.