Programok helyességének automatikus bizonyítása

OData támogatás
Konzulens:
Izsó Tamás
Hálózati Rendszerek és Szolgáltatások Tanszék

A programok fejlesztésének során használt dokumentációk és specifikációk kevésbé absztrakt formában, természetes nyelven íródnak és állnak a fejlesztők rendelkezésére. Mivel ez a fajta leírás bizonytalan és többértelmű, ezért nehéz eldönteni, hogy az így elkészített termék ténylegesen megfelel az elvárásoknak. Egyes programnyelvekben és programozási környezetekben lehetőség van mesterséges nyelven íródott, absztrakt leírást fűzni a forráskódba, aminek segítségével automatikusan is lehet ellenőrizni a kód helyességét a specifikáció alapján.

Az a lehetőség is előfordulhat, hogy nem szeretnénk a programhoz leírást fűzni, és az sem lényegi szempont, hogy a programunkat egy absztrakt leírásnak feleltessük meg, csupán a forráskódban szereplő esetleges szemantikai hibákat, a kód és tesztesetek futtatása nélkül meghatározhassuk. Ezt a módszert a program statikus analízisének hívják. Ezen a tudomány területen végzett kutatások széles köre bizonyítja, hogy léteznek algoritmusok és heurisztikák, amelyek képesek induktív módszerekkel a programozó által nehezen észrevehető, a programfejlesztés során keletkezett programozási hibákat felderíteni.

A statikus analízis csupán a programozó által szolgáltatott esetleges plusz információk által képes teljes körű programhelyesség bizonyítást kínálni, viszont erre nem mindig van szükség.

programhelyesség bizonyítást kínálni, viszont erre nem mindig van szükség.

Az alábbi szövegben bevezetésre kerülnek a parciális helyesség bizonyításával és induktív annotációk generálásárával kapcsolatos alapvető fogalmak és módszerek. Ezen metódusok főbb aspektusai egyszerű példákon keresztül kerülnek megvilágításra annak érdekében, hogy megalapozhassuk egy teljesen automatizált verifikációs fordító működését, és megvalósíthassuk annak a keretrendszernek az alapjait, aminek segítségével elvégezhetjük a programhelyesség bizonyítás feladatát. Ennek a keretrendszernek a felhasználásával C nyelven írt függvények parciális bizonyítását leszünk képesek támogatni.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.