Programhelyesség-bizonyítás fordítási időben

A dolgozat első tézise egy formális programmodellt vezet be haladási és biztonsági kritériumok megfogalmazására alkalmas temporális logikai operátorokkal. A modell levezetési szabályai bizonyítással együtt kerülnek bemutatásra. A bizonyított tételeken alapszik az az algoritmus, amely képes ellenőrizni a modellben felírt levezetések helyességét. A formális modell használatát egy Haskellbe ágyazott nyelv teszi lehetővé. Ennek kapcsán a dolgozat elemzi a Haskellben lehetséges nyelvbeágyazási technikákat. A megalkotott nyelv használatát a C++ egyes utasításainak specifikációja és egyszerű C++ programok levezetése demonstrálja. A második tézis a funkcionális nyelvek mintaillesztésének egy hiányosságával foglalkozik. Részletesen elemezi a beágyazott programokra történő mintaillesztés lehetőségeit funkcionális nyelvekben, és megmutatja, hogy ezek egyike sem nyújt kielégítő megoldást. A megoldás első lépése a korlátozott függvényminták fogalmának kidolgozása, amely a Curry nyelvből ismert függvényminták megszorítása. A korlátozott függvényminták szemantikája és implementációja a funkcionális nyelvek klasszikus mintaillesztésére visszavezethető. A korlátozott függvényminták alkalmasak a listaprefix minták, az n+k minták és a polimorf számliterálokra történő mintaillesztés egységes, konzisztens megvalósítására. A dolgozat bizonyítja, hogy a korlátozott függvényminta tulajdonság nem eldönthető. Ezért a megoldás második eleme az ellenőrizhető függvényminták bevezetése. Ez a fogalom egy döntési eljáráson alapszik, amely a korlátozott függvényminták egy szigorú részhalmazát fogadja el, és garantáltan terminál. Az elfogadott részhalmazban valamennyi korábban felsorolt használati eset benne van, és a döntési eljárás fordítóprogramokba beépíthető. A nyelvi kiterjesztés használata fordítóprogramba épített támogatás nélkül is haszálható egy függvénykönyvtár segítségével. A harmadik tézis a korábban bevezetett technikákat a formális szoftverfejlesztés egyes nemtriviális problémáinak megoldására használja. A dolgozat megmutatja, hogy a bizonyítások előállítására használt metaprogramozás biztonságos és hatékony eszköz. Bizonyítássablonokat ad egyes klasszikus matematikai bizonyítási technikákhoz és programkonstrukciók levezetési szabályaihoz. A kidolgozott rendszerben lehetőség nyílik dinamikus memóriát és mutatókat használó programok levezetésére az elválasztó logika hatékony bizonyítási stílusát használva. Axiomatizálhatók továbbá a C++ Standard Template Library konténereinek és bejáróinak műveletei