Pevný bod
je to stav programu, ktorý sa dalším vykonávaním programu uz nemení
definujme predikát FP pre program G:
- FP ? ? ?statement S: S in G ? S is x := E :: x = E ?
- FP[Rj] ? ? ?k: k ? j :: Rk.state = Rj.state ?
Príklady
1. k := k + 1
2. k := k + 1 if k < N
FP ? [k < N ? k = k + 1] ? k ? N
3. ? j: 0 ? j < N :: m = max(m, A[j]) ?, FP ?
? ?j: 0 ? j < N :: m = max(m, A[j]) ? ?
? ?j: 0 ? j < N :: m ? A[j] ? ?
m ? ? max j: 0 ? j < N :: A[j] ?