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。