specifications - Zed 规范：提升和应用一个操作多个模式

Question

我有一个Array跟踪模式序列的Data模式。使用提升，我可以提升Increment操作以使用Array.

ArrayIncrement里面只增加一个数据Array。我怎样才能使它每增加一次 ？Data\ran data

Answer 1

您增加所有值的方法中的基本障碍是，在 Promote （最后一行）中使用关系覆盖指定data'map 中的所有值都与data除了 position 之外的值相同index?。

一种方法是显式“迭代”所有元素的关系：

--- ArrayIncrement ---
| ΔArray
---
| dom data = dom data' 
| ∀ i:dom data; ΔData ·
|       θData = data i ∧ θData' = data' i ∧ Increment
------

在正文的第一行中，我们声明域保持不变，如果没有它，将有无限的解决方案和额外的元素。

在下一行中，我们设置变量来表示特定索引处的前后状态，类似于Promote解决方案中的第二行。