Спецификация Zed: продвижение и применение операции более чем к одной схеме

Question

у меня есть Array схема, которая отслеживает последовательность Data схемы. Используя продвижение, я могу продвигать Increment операция для использования с Array,

ArrayIncrement увеличивает только одно значение внутри Array, Как мне сделать так, чтобы он увеличивал каждый Data в \ran data?

Answer 1

Основным препятствием в вашем подходе к приращению всех значений является то, что использование реляционного переопределения в Promote (последняя строка) указывает, что все значения в data' сопоставить с тем же значением, что и в data кроме как в положении index?,

Один из подходов состоит в том, чтобы явно "перебрать" отношение для всех элементов:

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

В первой строке тела мы утверждаем, что область остается неизменной, без нее были бы бесконечные решения с дополнительными элементами.

В следующей строке мы устанавливаем переменные для представления состояния до и после по определенному индексу, аналогично второй строке в Promote вашего решения.