UNITY riešenia 2
Program P2
initially r = 0
assign r := f(r) r := g(r) r := h(r)
1: invariant (0 ? r) ? ?u(0 ? u ? z ? ?com(u))
ukázeme, ze na zaciatku je true a ze vykonanie hociktorého príkazu ho zachováva
2: FP ? r = f(r) ? r = g(r) ? r = h(r) t.j. FP ? com(r)
z 1 a 2 vyplýva, ze ak program dosiahne pevný bod, tak tento je najskorším casom stretnutia
Treba ešte ukázat, ze kazdé vykonanie programu vedie k pevnému bodu
3: Ukázeme, ze ak ?FP ? r = K v nejakom bode výpoctu, tak neskôr bude platit r > K
- z 1 vieme, ze r nemôze stúpat cez z, teda raz (angl. eventually) urcite bude musiet FP platit
- z 2 máme ?FP ? r = K ? K < f(K) ? K < g(K) ? K < h(K);
- nech K < f(K); ale raz sa r := f(r) musí vykonat a tak sa r zvýši