Szerdától volt Miskolcon OTDK, második helyezést értünk el :)
A dolgozat: Hoch Csaba és Tóth László Attila: Keretrendszer bizonyítottan helyes mobil kód támogatására, 2006.
(Az ilyen témák (bizonyítás, elő-utófeltétel, etc.) miatt volt is, aki megjegyezte:
"No, téged is asszimilált az ELTE"...)
Kicsit bővebben:
Java alapú a rendszer,
Adott az a probléma, hogy egy programnak (kódfelhasználónak) szüksége lenne komponensekre (mondjuk Java osztályokra), amelyeket letölthet, ámde nem garantált, hogy nem rosszindulatú. Ma is vannak aláírt programok - ekkor még nem biztos, hogy azt csinálja, amit várunk tőle, ezért kell a helyességét is bizonyítani. Erre már több modell is készült, az egyiket (CPPCC, Certified Proved-Proper
ty-Carrying Code) kibővítettük, és implementáltuk, egy keretrendszert készítettünk rá, ami a modell szereplőit valósjtja meg. Mivel helyességet kell bizonyítani, és számos szintaxis, különböző programozási nyelvek vannak, ezért előre nem lehet tudni, hogy hány különböző eset fordulhat elő, tehát a bizonyítást ellenőrző szereplőnek könnyen bővíthetőnek kell lennie (az is, hiszen egyetlen interfész egyetlen metódusát kell implementálni). A bonyolult a tényleges ellenőrzés, ami elbújik ez a metódus mögött.
A helyességbizonyítás meg azt jelenti, hogy adottak a kódra vonatkozó logikai állítások, és azt kell megvizsgálni, hogy ezeknek megfelel-e a kód (az implementációra igazaknak kell lenniük az állításoknak).