Najkratšia cesta 4
Dôkaz správnosti stratégie:
- metrika je ohranicená zdola a klesá, ak stav nie je FP ? FP sa nakoniec dosiahne
- v kazdom FP invariant platí, stací teda ukázat, ze matica, ktorá splna (1) a (2) je riešením problému
- nemáme cykly zápornej dlzky ? ?i, j ?najkratšia cesta s najviac N?1 hranami
- uvazujeme ?(x, y) také, ze najkratšia cesta z x do y má najviac m hrán. Indukciou podla m dokázeme, ze vzdialenost x, y je d[x, y]:
1. m = 1: triviálne d[x, y] = W[x, y]
2. nech tvrdenie platí pre m a nech najkratšia cesta z x do y má m+1 hrán. Predposledný vrchol tejto cesty nech je z, potom
- cesta x, z: m hrán
- cesta z, y: 1 hrana
podla indukcného predpokladu
- d[x, y] ? d[x, z] + d[z, y]
Program P1
initially ? || i, j :: d[i, j] = W[i, j] ?
assign ? i, j, k :: d[i, j] := min(d[i, j], d[i, k] + d[k, j]) ?