Programozás | Programozás-elmélet » Molnár András - Programhelyesség-bizonyítás

Programhelyesség bizonyitás Bp. 2001 november 15 Molnár András Alapfogalmak Algoritmus: • Egy jól megalapozott számítási eljárás, mely bemenete (input) egy érték vagy értékhalmaz, és létrehoz valamilyen értéket vagy értékhalmazt kimenetként (output.) [1] Más szavakkal az algoritmus felfogható, mint egy függvény, mely egy halmaz (input halmaz) elemeit képzi le egy halmaz (output halmaz) elemeire. P (x ) INPUT OUTPUT Program: • Az algoritmus egy implementációja. Ez lehet egy jól ismert programnyelven, pszeudó kódban, stuktogrammal, folyamatábrával vagy egyéb módon megvalósított algoritmus. Annak érdekében, hogy a program helyes működését belássuk, be kell vezetni néhány fogalmat. [2] Változók: • Input változók, azok a változók, melyek a program kezdőértékeit jelentik és a program futása során értékük nem változik. Jelölés: X = ( X 1, X 2,., Xn ) • Program változók, azok a váltózók, melyek a program

futása során átmeneti tárolóként szolgálnak. Jelölés: Y = (Y 1, Y 2,., Yn) • Output változók, azok a változók, melyek a program végrehajtásának befejezése során kapnak értéket. Jelölés: Z = ( Z 1, Z 2,., Zn) Input feltétel: • Az a feltétel, amely –egy adott program esetében- fenn kell, álljon (igaz kell, legyen) a kezdőértékekre ahhoz, hogy a program végrehajtható legyen. Jelölés: ϕ (X ) Output feltétel: • Az a feltétel, amely –egy adott program esetében- a program megállása után fenn kell, hogy álljon (igaz kell, legyen) az output változókra (eredményre). Jelölés: ψ ( X ,Y ) 2 • Program helyesség definíciói: 1. Megállás P program megáll ϕ mellett, ha minden olyan ξ input mellett, amelyre ϕ (ξ ) igaz, a program végrehajtása befejeződik. 2. Parciális helyesség P program parciálisan helyes ϕ-re és ψ-re nézve, ha minden olyan ξ inputra, amelyre ϕ (ξ ) igaz és a vele végrehajtott program megáll,

teljesül, hogy ψ (ξ , p (ξ )) igaz. 3. Totális helyesség P program totálisan helyes ϕ-re és ψ-re nézve, ha minden olyan ξ input mellett, amelyre ϕ (ξ ) igaz, a program megáll és ψ (ξ , p (ξ )) igaz. Bizonyítás célja: • Be kell bizonyítani, hogy minden, az input feltételnek megfelelő inputhoz tartozó végrehajtás esetén a program megáll, és a program végrehajtása után kapott output értékek kielégítik az output feltételt. Folyamatábra programok Minden program a következő öt elemből épül fel: 1. START utasítás, jelölése: START y ← f (x ) 2. ASSIGMENT utasítás, jelölése: y ← g (x, y) 3 3. TEST utasítás, jelölése: T t(x, y) F 4. HALT utasítás, jelölése: z ← h( x , y ) HALT 5. Csomópont, jelölése: Folyamatábra program: • Egy irányított gráf, mely csúcspontjaiban a fenti utasítások helyezkednek el. A gráf egy és csak egy START utasítást, valamint legalább egy STOP utasítást tartalmaz.

Minden utasítás rajta van a START utasítástól a STOP utasítások egyikéig vezető utak valamelyikén. Ez azt jelenti, hogy „zsákutca” nem szerepelhet a gráfban! 4 Parciális helyesség bizonyítása: START A ϕ(x1,x2): x2 ≠ 0 ( y1, y 2) ← ( x1, x 2) y1 ← ( y1 / y 2) z ← y1 B Ψ(x1,x2,z): x1 = z * x2 STOP 1. Vágási pontok meghatározása Az első (A) vágási pontot kezdő pontnak nevezzük és a START utasítás után kell elhelyezni, az utolsó vágási pontot (pontokat) a STOP utasítás (ok) előtt kell elhelyezni. A további vágási pontokat úgy kell meghatározni, hogy két vágási pont között mindig legyen hurokmentes út. Két pont közti szakaszokat rendre α, β, γ, stb. jelölésekkel látjuk el 2. Meghatározzuk az input ϕ ( X ) és outpu ψ ( X , Y ) feltételeket Ez feltételezi a program funkcionális ismeretét. 3. Minden vágási ponthoz meghatározunk olyan relációkat, melyek megmutatják az adott szakaszokon belül a

változók összefüggéseit. Ezen relációk meghatározásához célszerű az úgynevezett visszahelyettesítés módszert alkalmazni. 4. Felírjuk a helyességi feltételeket Ezek a feltételek azt állítják, ha a i-j szakasz kezdetén fennállt Pi, akkor a szakasz végén fennáll Pj. Végül bebizonyítjuk, hogy az összes helyességi feltétel igaz. 5 Visszahelyettesítés szabályai:  R( x , f ( x ))   r ( x , f ( x )) y ← f (x ) R(x, y)   r(x, y)  R ( x , g ( x , y ))   r ( x , g ( x , y )) y ← g ( x, y) R(x, y)   r(x, y) t ( x , y ) ∧ R ( x , y )  r(x, y)  t(x, y) T R(x, y)   r(x, y) ¬ t ( x , y ) ∧ R ( x , y )  r(x, y)  F t(x, y) R(x, y)   r(x, y) 6 Általános példa a visszahelyettesítésre:  R : t 1( x , g 1( x , y )) ∧ ¬ t 2 ( x , g 2 ( x , g 1( x , y )))  r : g 3 ( x , g 2 ( x , g 1( x , y )))  i y ←g1(x, y)  R : t 1( x , y ) ∧ ¬ t 2 ( x , g 2 (

x , y ))  r : g 3 ( x , g 2 ( x , y ))  T t1(x, y)  R : ¬ t 2 ( x , g 2 ( x , y ))   r : g 3 ( x , g 2 ( x , y )) y ← g 2( x , y )  R : ¬ t 2( x , y )   r : g 3( x , y ) F t2(x, y)  R :T   r : g 3( x , y ) y ← g 3( x , y ) j R :T  r:y 7 Példa a parciális helyesség bizonyítására: • A program számítsa ki két tetszőleges egész szám (X1;X2) hányadosát (Z). • Input: X1;X2 • Output: Z START A ϕ(x1,x2): x2 ≠ 0 ( y1, y 2) ← ( x1, x 2) y1 ← ( y1 / y 2) z ← y1 B Ψ(x1,x2,z): x1 = z * x2 STOP Bizonyítandó következtetés: • X2 ≠ 0 ⇒ X1 = Z*X2 Ez szavakkal kifejezve nem más, mint a kezdeti feltételből következik, hogy a kapott eredményt (Z) megszorozva az osztóval (X2), megkapjuk az osztandót (X1). Itt még nem tudjuk belátni, hogy az implikáció igaz! • Alkalmazzuk a visszahelyettesítést X2 ≠ 0 ⇒ X1 = Y1/Y2*X2 • Újra alkalmazzuk a visszahelyettesítést X2 ≠ 0 ⇒ X1 =

X1/X2*X2 Eljutottunk a program START utasításához. Itt már könnyű belátni, hogy az implikáció helyes, azaz a program parciálisan helyes. Észre kell venni, hogy ha a kezdeti megkötést (előfeltételt) nem vesszük figyelembe, akkor a program X2=0 esetében hibásan működne! 8 Maradékos osztás: • A program számítsa ki két tetszőleges természetes szám (X1;X2) hányadosának egészrészét (Z1) és maradékát (Z2). • Input: X1;X2 • Output: Z1,Z2 START ϕ ( X 1, X 2) : X 1 ≥ 0 ∧ X 2 > 0 A ( y1, y 2) ← (0, x1) B T (y1, y2) ←(y1+1, y2−x2) t( y2 ≥ x 2) F ( z1, z 2) ← ( y1, y 2) C STOP ψ(X1, X2, Z1, Z2): X1 = Z1X2 +Z2 ∧0≤ Z2 < X2 A program parciális helyességének bizonyítása a folyamatábrában szereplő hurok miatt közvetlenül nehézségekbe ütközik. A problémát a hurok felvágásával lehet megszüntetni Amennyiben a vágást a „B” pontban végezzük, úgy a programot reprezentáló gráf három,

hurokmentes útra bomlik fel. Mind a három út külön-külön elemezhető, amennyiben a „B” ponthoz is hozzárendelünk egy olyan relációt, amely leírja az adott pontban a változók kapcsolatát. Ez a reláció a következő lehet: X 1 = Y1X 2 + Y 2 ∧ Y 2 ≥ 0 Ezzel a relációval elértük, hogy mindhárom út egy relációval kezdődik, és egy relációval végződik. 9 Vegyük észre, hogy a „B” pontban lévő reláció az „A”-ból „B”-be vezető út, azaz az AB pontok által jelzett részprogram outputfeltétele, valamint a BB, illetve a BC részprogramok inputfeltételei! Most a teljes program parciális helyességének bizonyítása három részprogram parciális helyességének bizonyítására bomlik. Belátható, hogy a három részprogram kompozíciója útján a kiindulási programhoz jutunk! Az első (α) részprogram (AB) parciális helyességének bizonyítása: ϕ ( X 1, X 2) A ( y1, y 2) ← (0, x1) p( X 1, X 2.Y 1, Y 2) B Az α út

helyességi feltétele: ϕ ( X 1, X 2) ⇒ p( X 1, X 2, Y 1, Y 2) Behelyettesítés után: ϕ ( X 1, X 2) ⇒ p( X 1, X 2,01, X 1) azaz ( X 1 ≥ 0 ∧ X 2 > 0) ⇒ ( X 1 = 0 * X 2 + X 1 ∧ X 1 ≥ 0) Ez a következtetés nyilvánvalóan helyes. Az második (β) részprogram (BB) parciális helyességének bizonyítása: B T p( X 1, X 2.Y 1, Y 2) t( y2 ≥ x2) (y1, y2)←(y1+1, y2−x2) B p( X 1, X 2.Y 1, Y 2) 10 A β út helyességi feltétele: p( X 1, X 2, Y 1, Y 2) ⇒ p( X 1, X 2, Y 1, Y 2) Visszahelyettesítés után: p( X 1, X 2, Y 1, Y 2) ⇒ [(Y 2 ≥ X 2) ⇒ p( X 1, X 2, Y 1 + 1, Y 2 − X 2)] átírva: [ p( X 1, X 2, Y 1, Y 2) ∧ (Y 2 ≥ X 2)] ⇒ p( X 1, X 2, Y 1 + 1, Y 2 − X 2) Behelyettesítés után: [( X 1 = Y 1 X 2 + Y 2 ∧ Y 2 ≥ 0) ∧ (Y 2 ≥ X 2)] ⇒ [ X 1 = (Y 1 + 1) X 2 + (Y 2 − X 2) ∧ (Y 2 − X 2 ≥ 0)] Ez a következtetés helyes. A harmadik (γ) részprogram (BC) parciális helyességének bizonyítása: B t( y2 ≥ x 2)

p( X 1, X 2.Y 1, Y 2) F ( z1, z 2) ← ( y1, y 2) C ψ(X1, X2, Z1, Z2): X1 = Z1X2 +Z2 ∧0≤ Z2 < X2 A γ út helyességi feltétele: p( X 1, X 2, Y 1, Y 2) ⇒ ψ ( X 1, X 2, Z 1, Z 2) Visszahelyettesítés után: p( X 1, X 2, Y 1, Y 2) ⇒ [(Y 2 < X 2) ⇒ ψ ( X 1, X 2, Y 1, Y 2)] átírva: [ p( X 1, X 2, Y 1, Y 2) ∧ (Y 2 < X 2)] ⇒ ψ ( X 1, X 2, Y 1, Y 2) 11 Behelyettesítés után: [( X 1 = Y 1 X 2 + Y 2 ∧ Y 2 ≥ 0) ∧ (Y 2 < X 2)] ⇒ [ X 1 = (Z1 X 2 + Z 2) ∧ (0 ≤ Z 2 < X 2)] azaz [( X 1 = Y 1 X 2 + Y 2 ∧ Y 2 ≥ 0) ∧ (Y 2 < X 2)] ⇒ [ X 1 = (Y 1 X 2 + Y 2) ∧ (0 ≤ Y 2 < X 2)] Ez a következtetés is helyes. Miután bebizonyítottuk, hogy mindhárom programrészlet parciálisan helyes és mivel a három programrészlet kompozíciója az eredeti programot adja, belátható, hogy a maradékos osztást megvalósító program parciálisan helyes! Megállás bizonyítása: Itt azt kell bebizonyítani, hogy a program minden olyan

input esetében megáll, amely kielégíti az inputfeltételt. Ha a program nem tartalmazna hurkot, akkor a megállás triviális lenne. A problémát az okozza, hogy a hurokból a kilépés nem nyilvánvaló. Más szavakkal, azt kell belátni, hogy a számítás során mindenképpen elő fog fordulni olyan eset, amikor a végrehajtás nem a hurokban folytatódik. Ha a hurokból való kilépés további hurkok nélkül a végutasításhoz vezet, akkor a program megáll. A maradékos osztás programja esetében egy hurok van a folyamatábrában. Ennek vágási pontját „B”-vel jelöltük. A program inputfeltétele: ϕ ( X 1, X 2) : X 1 ≥ 0 ∧ X 2 > 0 A „B” ponthoz érve (függetlenül attól, hogy honnan, B-ből B-be, vagy A-ból B-be) mindig fennáll a váltózók pillanatnyi értékeire az alábbi reláció: q( X 1, X 2, Y 1, Y 2) : Y 2 ≥ 0 ∧ X 2 > 0 A fentiek alapján az alábbi két helyességi feltételt kell bizonyítani: Az α útra: ϕ ( X 1, X 2) ⇒ q(

X 1, X 2,0, X 1) és a β útra: [q( X 1, X 2, Y 1, Y 2) ∧ (Y 2 ≥ X 2)] ⇒ q( X 1, X 2, Y 1 + 1, Y 2 − X 2) 12 Behelyettesítve: ( X 1 ≥ 0 ∧ X 2 > 0) ⇒ ( X 1 ≥ 0 ∧ X 2 > 0) Ez nyilvánvaló! (Y 2 ≥ 0 ∧ X 2 > 0 ∧ Y 2 ≥ X 2) ⇒ (Y 2 − X 2 ≥ 0 ∧ X 2 > 0) Szintén triviális. Mivel a program a természetes számok halmazán működik, könnyű belátni, hogy a programváltozók is csak természetes számokat vehetnek fel. A „B” pontban mindig igaz, hogy X2>0. Vegyük észre, hogy “B”-ből “B”-be érkezve Y2 mindig csökken, továbbá tudjuk, hogy ezen a ponton igaz az Y2≥0! Ebből következik, hogy Y2 csökkenése nem történhet végtelen sok lépésen keresztül, más szavakkal a ciklus véges sok lépés után megáll! Totális helyesség Miután bebizonyítottuk, hogy • a program parciálisan helyes, • valamint megáll, megállapíthatjuk, hogy totálisan helyes! Irodalom [1] Thomas H. Cormen, Charles E

Leiserson, Ronald L Rivest, Algoritmusok, Műszaki Könyvkiadó1997, 1999 [2] Zohar Manna, Programozáselmélet, Műszaki Könyvkiadó1981 13