Global snapshots 5 ? Hlavná myšlienka
Ked sa príkaz daného programu vykoná, tak platí jedno z nasledujúcich:
- všetky premenné v danom príkaze sú zaznamenané,
- všetky premenné v danom príkaze sú nezaznamenané;
hodnota x môze byt zaznamenaná hocikedy potom, co bolo zaznamenávanie inicializované, a prv, nez sa vykoná príkaz obsahujúci x a nejaké uz zaznamenané hodnoty.
Tvrdenie: Kazdý program, ktorý implementuje R, splna predchádzajúci invariant.
Invariant platí, ked inicializujeme zaznamenávanie, za u, v vezmeme null.
Ukázeme, ze invariant sa zachová po vykonaní príkazu t, ktorý splna R.
- nech všetky premenné v t sú nezaznamenané a platí invariant pred vykonaním t. v obsahuje len premenné zaznamenané, teda v a t nemajú spolocné premenné. Môzu byt teda vykonané nezávisle na sebe;
- za u vezmime u;t
- za v vezmime v
- nech všetky premenné v t sú zaznamenané; potom partial sa nemení;
- za u vezmime u
- za v vezmime v;t