Najkratšia cesta, ASM 2
základom pre nasledujúci program je toto pozorovanie (pre zjednodušenie r znamená k[i, j]):
Teoréma: Z predchádzajúceho invariantu vyplýva:
(k[i, r] ? r ? k[r, j] ? r) ?
? min(d[i, j], d[i, r] + d[r, j]) ? H[i, j, r + 1]
Dôkaz. Z jednej z predchádzajúcich viet vieme, ze
H[i, j, k + 1] = min(H[i, j, k], H[i, k, k] + H[k, j, k])
- musíme teda ukázat, ze (k[i, r] ? r ? k[r, j] ? r) ? min(d[i, j], d[i, r] + d[r, j]) ? min(H[i, j, r], H[i, r, r] + H[r, j, r]); nasledovne:
d[i, j] ? H[i, j, r] /* z invariantu */
d[i, r] ? H[i, r, k[i, r]] /* z invariantu */
H[i, r, k[i, r]] ? H[i, r, r] /* z predpokladu */
d[i, r] ? H[i, r, r] /* z predošlých dvoch */
- podobne ukázeme, ze d[r, j] ? H[i, r, r]
Správnost nasledujúceho programu vyplýva z invariantu a z nasledujúceho:
FP ? ? ? i, j :: k[i, j] ? N ?