Programok analízise és szintézise

Megjegyzés: Fekete-fehér ábrákkal illusztrálva. ELŐSZÓ A szerző célja. A hatvanas évek végén ismerték fel a kutatók, hogy a program adott specifikáció szerinti helyessége tételszerűen megfogalmazható és bebizonyítható. Ennek a felismerésnek alapján jött létre a programozás módszertana, amely az elmúlt 10 év alatt a számítástudomány egyik legfontosabb fejezetévé vált. A programozási módszertan a programkészítés különböző fázisainak gyakorlati és elméleti kérdéseivel foglalkozik. A módszertan elméleti alapjainak tisztázása érdekében jelentős kutatómunka folyik az adatok és a programok szerkezetének, tulajdonságainak analizálása, valamint a programok automatikus előállítása területén. Ezek az eredmények, amelyek jórészt csak folyóiratokban találhatók meg, alkalmasnak látszanak arra, hogy a programozási módszertan gyakorlatát matematikailag megalapozzák. Könyvem megírásával ennek az elméletnek matematikailag megalapozott módszereit és bebizonyított tételeit kívánom eljuttatni az olvasóhoz. Vissza FÜLSZÖVEG A hatvanas évek második felében ismerték fel a kutatók, hogy a program adott specifikáció szerinti helyessége tételszerűen megfogalmazható és bebizonyítható. E felismerés alapján jött létre a programozási módszertan, amely az elmúlt tíz év folyamán a számítástudomány egyik legfontosabb fejezetévé vált. A kutatók egyre nagyobb aktivitással dolgoznak a programozási módszertan elméleti megalapozásán. A szerző ennek az elméletnek legfontosabb tételeit és módszereit kívánja eljuttatni az olvasóhoz. A könyv anyag három részből áll. Az elsőben a szerző az adatok programok szerkezetének, szerkezeti bonyolultságának elemzésével foglalkozik. A másodikban a programok logikai tulajdonságainak analizálására szolgáló legfontosabb módszereket ismerteti, külön tárgyalva azokat szekvenciális és párhuzamos programok esetén. A harmadik részben a programok szintézisével foglalkozik, azaz olyan módszereket ismertet, amelyekkel a program szövege automatikusan előállítható a program specifikációjából. TARTALOM Előszó 7 Matematikai alapfogalmak, jelölések 11 Adatszerkezetek analízise 19 Az adatelem és az adatszerkezet absztrakt fogalma 20 Alapobjektumok 22 Indexelt objektum, objektumhalmaz 23 Szekvenciális objektum, objektumlista 37 Láncolt objektum, objektumgráf, objektumfa, objektumlánc 40 Adatszerkezet-típusok formális definíciója 47 Feladatok 52 Programok szerkezetének analízise 54 A program matematikai fogalma 55 A program szerkezetének ábrázolása gráffal 58 A strukturált programszerkezet 63 A nem strukturáltság jellemzői 84 A program szerkezeti bonyolultsága 89 Szekvenciális nem determinisztikus és párhuzamos programszerkezetek 94 Feladatok 105 A szöveggel felírt program 109 Szekvenciális program, funkcionális rész 110 Adattípusok és deklaráció 114 Fastruktúrájú program 121 Feladatok 127 Szekvenciális programok funkcionális tulajdonságainak analízise 128 A programhelyesség alapfogalmai 129 A programhelyesség bizonyításának rendszere 130 Szekvenciális programok verifikációs módszerei 134 Invariáns állítások módszere (Floyd-módszer) 134 Részcélokra vonatkozó állítások módszere (Manna részcél-módszere) 152 Hoare deduktív módszere 158 Strukturális indukciós módszer (Burstall-módszer) 174 Kézi, automatikus és programmal támogatott bizonyítások 188 A módszerek összefoglaló értékelése 190 Feladatok 192 Nem szekvenciális programok analízise 197 Párhuzamos programok speciális tulajdonságai 198 Nem determinisztikus programok helyességének bizonyítása 203 Párhuzamos programok bizonyításának Owicki-Gried-módszere 216 Az irodalom áttekintése 225 Feladatok 226 Programok empirikus analízise 229 A programok statikus és dinamikus analízise 229 Programok kipróbálásának stratégiái 231 A próbaadatok előállítása 234 Összefoglalás és értékelés 244 Feladatok 245 Programszintézis 247 A programszintézis alapelvei 248 Strukturált programok szintézise 250 Absztrakt algoritmusok szintézise 275 Egy gráfbejáró absztrakt algoritmus szintézise 279 Konkrét gráfbejáró algoritmusok származtatása 289 A programszintézis összefoglaló értékelése 291 Feladatok 292 Irodalom 294 Névmutató 300 Tárgymutató 301