Najkratšia cesta 3: stratégia
Stratégia, formálny popis:
- na zaciatku d[i, j] := W[i, j]
- d[i, j] sa v priebehu výpoctu nezvyšuje, teda nemôze prekrocit W[i, j]
- invariant d[i, j] je dlzka nejakej cesty z vrcholu i do j ? d[i, j] ? W[i, j] (1)
- FP ? ? ?i, j, k:: d[i, j] := min(d[i, j], d[i, k] + d[k, j]) ? (2)
aby sme zabezpecili, ze vzdy dosiahneme FP, ukázeme, ze ak nejaký stav nie je FP, tak aspon jedno d[i, j] klesne. Metrika, ktorú pouzijeme, je nasledovná: suma ?d[i, j]. Kedze však niektoré hodnoty môzu byt ?, pouzijeme dvojice (num, sum) v lexikografickom usporiadaní, kde
- num = pocet (i, j) tak, ze d[i, j] = ?
- sum = ?+i, j: d[i, j] je konecné :: d[i, j]?
metrika je ohranicená zdola, kedze nemáme cykly so zápornou dlzkou ziadna váha nie je ??
Progress condition: metrika klesá, ak stav nie je FP:
?FP ? (num, sum) = (m, n) ? (num, sum) < (m, n) ?m, n (3)