如何在没有量词的情况下用 Z 表示法表示唯一属性？

Question

完全公开，这是大学课程。我不希望得到直接的答复，但我们将不胜感激。

我需要使用 Z 表示法为 Item 实体建模。这是描述：

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.

部分要求是对这些实体建模没有量词。

这就是我最后的结果，但我不确定它是否正确：

Schema for Item

想法是名称是字符串的某种组合，ID 是正整数和所述名称的元组，价格和类别都映射到总函数。

第一个谓词是为了确保价格为正，第二个谓词是为了确保ID的唯一性，即将域缩减为所有尚未分配的整数。 不过我认为这不正确。

Answer 1

您的方法的主要问题是您试图将有关整个系统（或部分系统）的信息放入单个项目的描述中。例如。您将价格指定为从 id 到 float 的映射 - 原则上这很好 - 但您没有为每个项目提供这样的功能。

有很多方法可以指定它，我展示两种方法：

您有两个架构：例如Item 和 Database
```
+-- Item -----
| id: ℕ
| name: String
| price: ℝ
| category: String
|----
| price ≥ 0
+----------

+-- Database -----
| items: ℕ +-> Item
|----------
```
这样您就可以将每个项目的 ID 从项目本身移走。当每个项目也有一个字段 id 时，在没有量词的情况下陈述 items 应该将一个 id 映射到具有相同 id 的项目这一事实会很复杂。或者，当您只使用一组项目时，如果没有量词，很难描述两个项目必须具有不同的标识符。

每个项目的 id 的唯一性由 items 作为一个函数来保证。

或者只对项目的每个方面使用几个函数：
```
+-- Items -----
| ids: ℕ
| name: ids --> String
| price: ids --> ℝ
| category: ids --> String
+----------
```
但是要说明所有价格都必须是非负的且没有量词这一事实是很困难的。也许通过将 ℝ 替换为 { x:ℝ | x≥0}.

一般性评论：您需要使用您的 ID 进行计算吗？也许你可以引入一个带有 [ID] 的类型。这同样适用于类别（例如 [CATEGORY]）。

名字不是一个字符串吗？但我不认为它会是一组（无序的）字符串。

如何在没有量词的情况下用 Z 表示法表示唯一属性？

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

formal-methods

z-notation