spécification Zed: Promotion et appliquer une opération plus d'un schéma

Question

I ont un schéma Array qui garde la trace de la séquence de Data schémas. En utilisant la promotion, je suis en mesure de promouvoir Increment opération à utiliser avec Array. Incrémente seulement une donnée à Array. Comment puis-je faire en sorte qu'il incrémente tous lesData dans \ran data?

Answer 1

L'obstacle fondamental dans votre approche pour augmenter toutes les valeurs est que l'utilisation de la commande relationnelle dans la promotion (dernière ligne) précise que toutes les valeurs de data' carte à la même valeur que dans data sauf à la position index?.

Une approche est explicitement « itérer » sur la relation pour tous les éléments:

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

Dans la première ligne du corps, nous affirmons que le domaine reste le même, sans qu'il y aurait une infinité de solutions avec éléments supplémentaires.

Dans la ligne suivante, nous configurons les variables pour représenter l'état avant et après à l'index spécifique de façon analogue à la deuxième ligne dans Promote de votre solution.