formal-methods - 如何为这种情况正确设计 Z 模式？

Question

我发现的所有示例都只有 2 个声明such as name and date OR members and telephone。但是，我的情况是这样的：

我想创建一个名为 AppointmentDB 的 Z 模式。AppointmentDB 保留约会的详细信息，例如目的、参加者和日程安排

---

我的看法（已编辑）：

有 5 个声明和 1 个谓词

|--AppointmentDB----------------
|attendees : P Person
|appointments : P APPOINTMENT
|hasAppointment : Person ↔ APPOINTMENT
|schedule : APPOINTMENT → DateTime
|purpose : APPOINTMENT → Report 
|-----------------------------
|attendees ⊆ dom(hasAppointment)
|-----------------------------

如您所见，我正在尝试将 APPOINTMENT 链接到它的所有其他属性。我的架构是否正确或完整，或者如何进一步优化它？另外，我怎么知道我应该从关系中考虑哪个关系来定义谓词部分？

Answer 1

purpose在您的规范中，例如和之间没有链接schedule。您schedule以一种方式定义一个人被映射到任意次数，目的将一个人映射到任意数量的单词。但是没有办法知道这个人在什么时间有什么目的的约会。

我想你想要一个约会有时间和目的。我的建议（实际上有很多方法可以实现这一点）是为约会引入一种数据类型，例如使用运营商集：

[APPOINTMENT]

然后你可以指定一个人有任意数量的约会：

|--------------------
| appointments: P APPOINTMENT
| hasAppointment: Person <-> APPOINTMENT
|----
| appointments = ran(hasAppointment)
|--------------------

对于每个约会，您可以指定其时间和目的：

|--------------------
| schedule: appointments --> DateTime
| purpose: appointments --> Word
|--------------------

因此，这不是您在架构中指定的所有内容，但我不确定如何准确解释例如object或availability您的规范。但我认为让约会本身成为对象的基本方法在大多数情况下都会有所帮助。

另一种不引入类型的APPOINTMENT方法是定义模式Appointment并将其用作记录数据类型。