Global snapshots 6
V okamihu, ked sa inicializuje zaznamenávanie (begun ? true) platí
init = cur ? partial = cur
teda invariant platí pre u = v = null.
Predpokladajme, ze invariant platí pre nejaké u, v a nejaký výpocet. Budeme uvazovat 3 prípady, kedy sa môze menit partial alebo cur.
Prípad 1: ak sa zaznamená premenná, tak sa nemenia hodnoty partial alebo cur a teda môzeme zobrat pôvodné u, v.
Teraz budeme uvazovat, ze sa vykoná prílaz t. Nech cur’ je stav pred vykonaním t a cur je stav po vykonaní t.
[init] u [partial’] ? [partial’] v [cur’]
Musíme nájst u’, v’ tak, aby platilo
[init] u’ [partial] ? [partial] v’ [cur]
(Vykonanie t neovplyvnuje x.done alebo x.rec.)