Algoritmusok helyességének bizonyítása A Floyd-módszer
Algoritmusok végrehajtása • Egy A algoritmus esetében a változókat három változótípusról beszélhetünk, melyeket az X, Y és Z vektorokba csoportosítjuk a következőképpen: • X = (X1,X2,…Xn) – bemeneti változók (ismerteknek tekinthetőek) • Z = (Z1,Z2,…Zo) – az algoritmus által kapott eredmények • Y = (Y1,Y2,…Yp) –a köztes eredmények eltárolására használt változók
• A V = (V1,V2,…Vk) – vektor ezek egyesítése, mely az algoritmus összes változóját tartalmazza • A végrehajtás bármely pillanatában, minden változónak lehet egy adott értéke, vagy még nem inicializált. • Az A algoritmus állapotának nevezzük azt az s = (a1,a2,…ak) vektort, amely az algoritmus k változójának aktuális értékeit tartalmazza • Amennyiben egy Vj változó még nem inicializált, az aj érték ismeretlen (jelölés: ?) • Az algoritmus által végrehajtott számítást az s0,s1,…,sm állapotsor határozza meg (s0 – kezdeti állapot, sm – futás utáni végállapot)
Algoritmusok végrehajtása • Példa: osztók számának meghatározása •
Az algoritmus: •
BEGIN NoDivisors • READ X; • Y:=2; • Z:=0; • WHILE X>Y DO • IF X mod Y = 0 THEN Z:=Z+1 ENDIF • Y:=Y+1; • ENDWHILE • WRITE X, Z
•
•
END NoDivisors
Az algoritmus által végrehajtott számítás: s0=(?,?,?) P1(s0) = s1 = (6,?,?) P2(s1) = s2 = (6,2,?) P3(s2) = s3 = (6,2,0) P4(s3) = s4 = (6,2,1) P5(s4) = s5 = (6,3,1) P6(s5) = s6 = (6,3,2) P7(s6) = s7 = (6,4,2) P8(s7) = s8 = (6,4,2) P9(s8) = s9 = (6,5,2) P10(s9) = s10 = (6,5,2) P11(s10) = s11 = (6,6,2) P12(s11) = s12 = (6,6,2)
Legyen D az X bemeneti vektor által felvehető értékek halmaza. Egy adott i∈D bemenetre az A algoritmus egy s végállapotban fejeződik be. A Z kimeneti vektorban kapott értékek az A algoritmus i bemeneten végrehajtott számításainak eredménye. Ha az R halmaz az összes lehetséges eredmények halmaza, az A algoritmus egy A:D→R függvényként értelmezhető.
Algoritmusok helyessége • Egy program helyes, ha megfelel a specifikációnak, azaz azon bemenetekre, amelyek megfelelnek a specifikációknak, a program futtatása helyes eredményekhez vezet. A helyesség ellenőrzésekor nem vesszük figyelembe más szempontokat (pl. komplexitás stb.) • Egy probléma nem értelmezhető bármilyen bemenetre. A ϕ(X) bemeneti predikátum (prekondíció/előfeltétel) határozza meg azokat a bemeneteket, amelyekre a probléma értelmezhető. (a program futtatásának csak az előfeltételt teljesítő X bemenetekre van értelme) • Az X bemeneti értékek és Z eredmények között kapcsolatok állnak fent, melyet a ψ(X,Z) kimeneti predikátum (postkondíció/utófeltétel) ad meg. Ez az X és Y vektor azon a és b értékeire igaz, melyek esetében az a bemenetre kapott eredmény b. Ha a bemeneti adatokra futtatva a programot b’ eredményeket kapunk és ψ(a, b’ ) hamis, akkor a kapott eredmények nem helyesek. • A program specifikációja megadható a fenti két predikátum által (az X és Z vektoroknak ismerteknek kell lenniük). • Példa: az r négyzetgyök kiszámítása: ϕ(X): „x>0”; ψ(X,Z)> “r2=x” • Programozók számára is helyesen: ϕ(X): „x>0 ∧ ε>0”; ψ(X,Z)> “ |r2-x| < ε”
Algoritmusok helyessége • Def. 1: A P program megáll ϕ-re nézve, ha minden olyan x inputra, amelyre ϕ(x) teljesül, P(x) definiált. • Def. 2: A P program parciálisan helyes ϕ-re és ψ-re nézve, ha minden olyan x inputra, amelyre ϕ(x) teljesül és P(x) definiált, ψ(x,P(x)) teljesül. • Def. 3: A P program totálisan helyes (teljesen helyes) ϕ-re és ψ-re nézve, ha minden olyan x inputra, amelyre ϕ(x) teljesül, P(x) definiált, és ψ(x,P(x)) teljesül. Másképpen: A P program totálisan helyes a probléma specifikációjára nézve, ha megáll és parciálisan helyes az illető specifikációra nézve • Megjegyzések: • a parciális helyesség ellenőrzése a fontosabb, ha a program nem áll le azt észrevesszük… • A továbbiakban „helyességen” a totális helyességet értjük
Algoritmusok helyessége • Példák Két szám közül a nagyobbik meghatározása: FUNCTION MAX(x,y) IF x≤y THEN MAX:=y ELSE MAX:=x ENDIF END MAX Helyes: - nem tartalmaz ciklust, tehát biztosan véget ér - A ψ:=(MAX≥x) ∧ (MAX≥y) ∧ ((MAX=x) ∨ (MAX=y)) kimeneti feltétel igaz
Két vektor elemeinek összehasonlítása: FUNCTION EQUAL(n,X,Y) i:=1 WHILE i≤n DO IF xi=yi THEN EQUAL:=TRUE ELSE EQUAL:=FALSE ENDIF ENDWHILE END EQUAL Nem helyes: - nem ér véget, mivel az i értéke nem módosul - ha kiegészítjük az i:=i+1 megfeleltetéssel: nem parciálisan helyes: pl. n=2, X=(5,55) és Y=(9,55) –re TRUE
A Floyd módszer a helyesség bizonyítására • Floyd 1968: az induktív állítások módszere • Vágási pontok elhelyezése a programban: • egy vágási pont az elejére (a beolvasás után) • egy-egy vágási pont minden ciklushoz • egy vágási pont a végére • Komplexebb esetben: egy-egy vágási pont minden minden alprogram -ba/-ból történő be/ki –lépéshez • Mindenik vágási ponthoz hozzárendelünk egy induktív állítást (predikátumot): a bemeneti vágási pontnál ez ϕ(X), a kimenetinél ψ(X,Z) • Egy (i,j) vágási pont pár esetében több út vezethet i-ből j-be. Az olyan α utakat vesszük figyelembe, amelyek nem tartalmaznak más vágási pontokat. • Rα(X,Y) –al jelöljük azt a predikátumot, ami az út bejárásának feltételét adja • rα(X,Y) –al jelöljük a függvényt, mely az illető úton az Y közbeeső változókra alkalmazott transzformációkat adja.
A Floyd módszer a helyesség bizonyítására
• Mindenik úthoz hozzárendelhető egy ellenőrzési feltétel: ∀ X ∀ Y (Pi(X,Y) ∧ Rα(X,Y) → Pj(X, rα(X,Y))) azaz: ha a i indulási pontban a Pi igaz és az i, j pontok közötti α út bejárása megtörténik, a j érkezési pontnak megfelelő Pj feltétel igaz. • Tétel 1: Ha minden ellenőrzési feltétel igaz, akkor a P program parciálisan helyes a ϕ(X) és ψ(X,Z) által megadott specifikációra (a bizonyítás a logikai implikáció tranzitivitásán alapszik, valamint azon, hogy a kezdeti pont ellenőrzési feltétele ϕ(X), a végponté ψ(X,Z).
A Floyd módszer a helyesség bizonyítására • Példa: legnagyobb közös osztó •
PROCEDURE LNKO(n1,n2,d) {A: PA: ϕ(X): n1∈N ∧ n2∈N} d:=n1; i:=n2; WHILE (d≠i) and (i>0) DO IF d>I THEN d:=d-i; ELSE i:=i-d; ENDIF ENDWHILE
{B: PB: (d,i)=(n1,n2)}
{C: PC: ψ(X,Z): d=(n1,n2)} END LNKO
• A használt változók: X=(n1,n2), Y=(d,i), Z=(d)
A Floyd módszer a helyesség bizonyítására • A megfelelő utak bejárásának feltételei: • Rα1(X,Y) = (d≠ i) ∧ (i>0) • Rα2(X,Y) = (d≠ i) ∧ (i>0) ∧ b • Rα3(X,Y) = not ((d≠ i) ∧ (i>0)) ↔ (d=i) ∨ (i=0)
• B logikai kifejezés, amely az IF két ágától függ • Az α2 út tulajdonképpen két másik egyesítése (a d
i esetek) • Az utaknak megfelelő transzformációk: • rα1(X,Y) = (n1,n2) • rα2(X,Y) = if d>i then (d-i, i) else (d,i-d) • rα3(X,Y) = rα2(X,Y)
• Az utaknak megfelelő ellenőrzési feltételek: • Cα1= (n1 ≠ n2) ∧ (0 ≠ n2) → ((n1,n2)=(n1,n2)) • Cα2= ((d,i)=(n1,n2)) ∧ (d≠ i) ∧ (i ≠ 0) → ((d>i) ∧ (d-i,i) =(n1,n2)) ∨ ((d
A Floyd módszer a helyesség bizonyítására • Def. 4: Egy (W,<) parciálisan rendezett halmazt megalapozottnak nevezünk, ha nincs benne végtelen csökkenő sorozat. • Megállás ellenőrzéséhez bevezetett feltételek: az egyik vágási pontból a másikba történő eljutás során egy választott megalapozott halmazon bizonyos függvények értéke csökken (következéséképpen nem járhatunk végig egy utat végtelenszer, tehát a program megáll) • Minden i vágási ponthoz egy ui: DX×DY →M függvényt rendelünk • Az α útra a megállási feltétel a következő: ∀ X ∀ Y (Pi(X,Y) ∧ Rα(X,Y) → ui(X,Y)>uj(X, rα(X,Y))) • Tétel 2: Ha minden megállási feltétel igaz, akkor a P program megáll a ϕ(X) specifikációra. (raa módszerrel bizonyítható: ha feltételezzük, hogy a program nem áll le, akkor egy végtelen csökkenő sorozatot kapunk, ami ellentmond a megalapozott halmazzal)
A Floyd módszer a helyesség bizonyítására • Az LNKO példa vágási pontjaihoz kiválasztjuk a következő függvényeket: • u1(X,Y) = 2*n1 + 2*n2 • u2(X,Y) = d+i • u3 = 0;
• Az utaknak megfelelő megállási feltételek: • Tα1 = (n1≠n2) ∧ (n2>0) → (2*n1 + 2*n2) > n1 + n2 • Tα2 = (PB ∧ (d>i) ∧ (i>0) → d+i>d) ∨ (PB ∧ (d0) → d+i>i) • Tα3 = TRUE
• Ellenőrizhető, hogy mindhárom feltétel teljesül n1>0 –ra, de Tα2 hamis, ha n1=0, mivel d értéke 0 lesz és az i>i hamis. Ebben az esetben az α2 út végtelenszer lenne bejárva, mivel d és i értéke nem módosulna az út bejárása során. • Ahhoz, hogy egy totálisan helyes algoritmust kapjunk, úgy kell módosítanunk az LNKO algoritmust, hogy ne lépjen be az α2 útra, ha d=0
A Floyd módszer a helyesség bizonyítására • Példa: legnagyobb közös osztó •
PROCEDURE LNKO(n1,n2,d) IF n1=0 THEN d:=n2; i=0; ELSE d:=n1; i:=n2; WHILE (d≠i) and (i>0) DO IF d>I THEN d:=d-i; ELSE i:=i-d; ENDIF ENDWHILE END LNKO
• A használt változók: X=(n1,n2), Y=(d,i), Z=(d)
{A: PA: ϕ(X): n1∈N ∧ n2∈N}
{B: PB: (d,i)=(n1,n2)}
{C: PC: ψ(X,Z): d=(n1,n2)}
