Zed specification: Promotion and applying an operation more than one schema

Question

I have an Array schema that keeps track of sequence of Data schemas. Using promotion, I am able to promote Increment operation to use with Array.

ArrayIncrement only increments one data inside Array. How do I make it such that it increments every Data in \ran data?

Answer 1

The basic obstacle in your approach to increment all values is that the use of the relational override in Promote (last line) specifies that all values in data' map to the same value as in data except at position index?.

One approach is to explicitly "iterate" over the relation for all elements:

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

In the first line of the body we state that the domain stays the same, without it there would be infinite solutions with additional elements.

In the next line we set up the variables to represent the before and after state at the specific index analogously to the second line in Promote of your solution.