formal-methods - Z 表示法：序列的序列 - 求和

Question

我只想说这是一个大学项目。我不期待答案，而是更多的“提示”。

我有一个包含一系列队列的超市模式：

+-- Supermarket-------
|queues: seq Queue
----------------------

这是我定义队列的方式：

+-- Queue ----------
|length: ℕ
--------------------

我希望定义一个模式来返回排队等候的客户总数。到目前为止，我有：

+--TotalQueueCustomers----
|Ξsupermarket: Supermarket
|totalCustomers!: ℕ
|-------------------------
|totalCustomers = total θ supermarket
--------------------------

我正在努力定义total函数。它需要“循环”每个队列中的每个客户并对他们length的 s 求和。这是我到目前为止所拥有的：total = q: Queue ⦁ q.length ↦ q.length

任何想法？

Answer 1

您可以通过具有基本情况（无队列）并指定如何计算附加队列来归纳定义函数：

total: seq Queue → ℕ
---
total(∅) = 0
∀ q: Queue; qs: seq Queue ⦁ total( <q> ^ qs ) = q.length + total(qs)

<q>是具有单个元素的序列q，a ^ b表示序列连接运算符（Z 参考手册的第 4.5 节）。

（请注意：我没有使用 Z 类型检查器检查此示例，因此它可能包含某种语法错误 - 但想法应该很清楚）