Zed的规范：促进和应用操作一个以上的架构

Question

我有一个Array模式，它跟踪的Data模式序列。使用促销，我可以促进Increment操作使用Array。

ArrayIncrement只在Array内增加一个数据。我该如何使它在\ran data中每增加Data？

Answer 1

在你的方法，以增加所有值的基本障碍是，在促进（最后一行）使用关系覆盖的规定，除了在index?位置data'映射到相同的值data所有值。

一种方法是明确的“循环”上的所有元素的关系：

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

在我们规定的域保持不变身体的第一线，没有它会有有无穷多解额外的元素。

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