specifications - Zed 仕様: 複数のスキーマの昇格と操作の適用

Question

Arrayスキーマのシーケンスを追跡するスキーマがありますData。Incrementプロモーションを使用して、 で使用する操作をプロモーションできArrayます。

ArrayIncrement内の 1 つのデータのみをインクリメントしますArray。ごと Dataにインクリメントするようにするにはどうすればよい\ran dataですか?

Answer 1

すべての値をインクリメントするアプローチの基本的な障害は、プロモート (最後の行) でリレーショナル オーバーライドを使用すると、position 以外のすべての値data'が同じ値にマップされるように指定されることです。dataindex?

1 つのアプローチは、すべての要素の関係を明示的に「反復」することです。

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

本文の最初の行では、ドメインが同じままであると述べています。それがなければ、追加の要素を含む無限のソリューションが存在することになります。

次の行では、ソリューションの 2 行目と同様に、特定のインデックスで前後の状態を表す変数を設定しPromoteます。