Výpoctový model
mnozina výpoctových postupností priradená ku kazdému programu
nekonecné postupnosti, kazdá reprezentuje jeden mozný beh (výpocet) programu
Rj = j-ty prvok postupnosti R, j ? 0
Rj = (Rj.state, Rj.label)
state (stav) ? hodnota všetkých premenných
label ? príkaz vykonaný v j-tom kroku
R0.state ? iniciacný stav (ak nie sú dané iniciacné hodnoty pre všetky premenné, nemusia byt rovnaké pre rôzne R)
Rj+!.state je jednoznacne urcený Rj.state a Rj.label-om, teda R0.state a { Rk.label | 0 ? k < j } urcujú Rj.state
Spravodlivý výber príkazov: ?R?S, Rj.label = S pre nekonecne vela j
p[Rj] = p platí v stave Rj.state
{p} S {q} znamená
?R?j: (p[Rj] ? Rj.label = S) ? q[Rj+!]