UNITY

Unbounded Nondeterministic Iterative Transformations

• Programy:

  • deklarácie premenných
  • špecifikácia pociatocných hodnôt
  • mnozina priradení

• Vykonanie:

  • zacína zo stavu vyhovujúceho vstupnej (pociatocnej) podmienke
  • program sa vykonáva donekonecna
  • v kazdom kroku sa nedeterministicky vyberie priradovací príkaz a ten sa vykoná
  • kazdý príkaz sa vyberie nekonecne vela krát

• Nešpecifikuje sa:

  • kedy sa príkaz vykoná
  • kde sa vykoná

• Programy sa dalej alokujú na konkrétne architektúry, kde sa uz špecifikuje viac

• Stav sa volá pevný bod, ak vykonaním lubovolného príkazu program prejde do toho istého stavu

• predikát FP charakterizuje pevný bod

• stabilný predikát je taký, ktorý ked raz platí, platí potom uz stále

• (Pozor: angl. eventually znamená urcite niekedy/raz iste)

• (FP je stabilný)

Previous slide

Next slide

Back to first slide

View graphic version