Bevezető
Programok készítése során legtöbbször elégségesnek tűnik ’pusztán’ a feladat megoldó algoritmusának lekódolása. Nyilvánvaló, szinte említést sem érdemel, hogy az elterjedt programozási nyelvek ezt a megközelítést támogatják. Azonban számos esetben indokolt lehet, hogy olyan programokat készítsünk, melyek biztosan és helyesen oldják meg a kitűzött feladatot. Ahhoz hogy ezek a kritériumok teljesíthetők legyenek, már nem elegendő csak az algoritmus lekódolása, ebben az esetben már a feladatot (vagy részfeladatokat) is valamilyen absztrakt formában le kell írni. Feladatok leírása több módszer is létezik, egyik ilyen elterjedt módszer a feladat elő- és utófeltételes specifikálása (és a hozzátartozó invariáns állítások alkalmazása). Manapság már számos olyan programozási nyelvet kiegészítő eszköz van, amely a programhelyesség-ellenőrzésben ezeket a módszereket használja, azonban kevés az olyan nyelv, ahol magába a nyelvbe van beleintegrálva ez a képesség. Ezért érdekes az Eiffel programozási nyelv, mely nem csupán magában foglalja ezeket a képességeket, hanem egész szerkezetét - vagy ha úgy tetszik a nyelv filozófiáját – áthatja a programhelyesség kérdése. Az Eiffel programhelyesség fogalmának kialakítását a következők szerint tárgyaljuk, elsőként a szükséges alapismereteket tekintjük át röviden, majd a nyelvi elemek ismertetése következik. A nyelvi elemek tulajdonképpen azok a részek amelyekre a program helyesség építhető. A részek tárgyalása után vizsgáljuk meg az egész program helyességet, ami az addig ismertetett fogalmakra és nyelvi elemekre épül.
Helyességi specifikációs nyelv
Az Eiffel nyelv helyességi specifikációja alatt a nyelv egy bizonyos részét értjük, mely elsősorban logikai kifejezésekre épül. Ezek a kifejezések deklaratív módon fogalmazzák meg a program működését.
A specifikációs nyelvek többnyire az elsőrendű logikára épülnek. Az elsőrendű logikai formulák segítségével könnyen megfogalmazhatók olyan állítások, melyek a program működését deklaratív módon adják meg. Az Eiffel specifikációs nyelvében definiálhatunk egy halmazt, un. jól formált formulákat, mely halmazból választott formulákat megadhatunk a helyességi specifikációkban. Ez a jól formált formula halmaz nem azonos az elsőrendű logika (más néven predikátumlogika) jól formált formula halmazával, sőt még kölcsönösen egyértelmű – bijektív – megfeleltetés sem létesíthető a kettő között. Például nem használhatók az Eiffel helyességi specifikációban az 
(egzisztenciális) és 
(univerzális) kvantorok. Hasonló konstrukciók függvények és ciklusok együttes alkalmazásával valósíthatók meg. Jól formált formulákkal logikai állításokat fogalmazunk meg. A logikai állítások BOOLEAN típusú kifejezések, melyek a program bizonyos pontján lévő logikai összefüggéseket írnak le. Ezek az összefüggések vonatkozhatnak attribútumokra, helyi változókra, vagy függvények visszatérési értékeire. A logikai állítások nem csak helyességi specifikáció alapját képezve írják le a program működését, hanem egyben elősegítik a program megértését és dokumentálását. Amennyiben megadunk egy logikai kifejezést, mint specifikációt, ezzel tulajdonképpen program működésével szemben támasztott óhajunkat fejezzük ki. Ha a program egy adott pontján a logikai kifejezés nem teljesül, akkor a program nincs összhangban az óhajunkkal, tehát a specifikációval.
Az Eiffel helyességi specifikációs nyelvének megismerése előtt még néhány további ismeretet célszerű feleleveníteni.
Hoare-formulák
Ha adott egy M művelet annak E előfeltétele és U utófeltétele, akkor az { E } M { U } hármast Hoare-formulának nevezzük. A formula akkor igaz, ha E előfeltétel az M művelet végrehajtása előtt igaz és ha az M műveletet végrehajtjuk, akkor az befejeződik és végrehajtása után az U utófeltétel igaz lesz. Ez az értelmezés az úgynevezett teljes helyesség fogalmát írja le. Létezik ennél gyengébb definíció is, mely nem követeli meg az M művelet befejezését, ekkor részleges helyességről beszélünk.
Az { E } M { U } Hoare-formula elő- és utófeltételekből álló
{ ¬verem.tele } verem.berak(uj_elem) { verem.elem = uj_elem }
Ami azt jelenti, hogy ha a verem nincs tele, akkor a berak művelet befejeződik és a végrehajtás az új elem a verem tetején helyezkedik el.
Az általánosan ismert Hore-formulákhoz további fogalmak ismeretére van szükség. Most a legegyszerűbb úgy fogalmaznom, hogy aki az ELTE programozó matematikus szakára járt, annak a ’Bevprog’ (pontosabban, bevezetés a programozásba vagy programozás módszertan) tárgyban tanult fogalmak jelennek meg a helyességi specifikációs nyelvben. Persze, a fogalmak máshol is ismertek, megtalálhatók, azonban a bevprog ismeretekkel egy fogalom megértése sem okoz gondot.
Előfeltétel, utófeltétel
A Hore-formulában is megjelenő E előfeltétel alkalmas annak a kifejezésére, hogy egy bizonyos programrészlet lefutásához milyen előzetes feltételezésekkel élünk, például egy osztás előfeltétele, hogy a nevező nem lehet nulla vagy egy üres veremből nem lehet törölni, így a törlés művelet előfeltétele az, hogy a verem ne legyen üres. Teljesen analóg az utófeltétel jelentése, miután egy programrész lefutott a bizonyos dolgokat elvárunk vagy garantálunk, mint a lefutott program hatása. Például egy verembe történő berakás művelet hatása, ha nem teli a verem, akkor a verem tetején a berakott elemnek kell lennie. Bevprogosoknak, csak emlékeztetőül Q: ( … ), R: ( … ) Most nézzünk egy példát, hogyan kell megadni az elő- és utófeltételeket Eiffelben, egy verem adatszerkezet berak műveletének szerkezete:
bereak (e: G) is
require
nincs_tele: not tele
do
elemszam := elemszam + 1
tomb.put (e, elemszam)
ensure
uj_elem_a_tetejen: elem = e
nem_ures: not ures
…
end
Az előfeltételeket require (követel), míg az utófeltételeket az ensure (biztosít) kulcsszavak vezetik be. Az elő- és utófeltételek megadása nem kötelező, ha nem adjuk meg akkor alapértékük a True logikai formula lesz.
Az Eiffel megengedi, hogy a logikai állításoknak nevet adjuk, például:
haromszog_vagy_negyszog: csucsszam = 3 or csucsszam = 4
Azon kívül az Eiffel nyelv lehetőséget biztosít a logikai állítások blokkba, csoportba való szervezésére. Logikai állítások csoportján egy vagy több logikai állításnak a forráskódban szereplő fizikai sorrend alapján történő felsorolását értjük. Ezeket logikai állításokat, bár ez nem jelölt, az and then logikai művelet kapcsolja össze.
Speciális elemek
Old
Az utófeltételekben, ahol a programrész hatását írjuk le, a logikai kifejezésekben gyakran van szükség egy változó korábbi értékére, erre ad megoldást az old szerkezet. Az old mögött egy kifejezés állhat. A szerkezet hatásköre az adott eljárásra terjed ki. Ha az elemszam a veremben éppen tárolt elemek számát jelenti, akkor egy verem töröl műveletére egy példa:
-- Aktuális elem törlése.
torol is
require
nem_ures: not ures
do
elemszam := elemszam –1
ensure
elemszam_csokkent:
elemszam = old elemszam – 1
ures_ha_egy_elem_volt:
old elemszam = 1 implies ures
nincs_tele:
not tele
end
Az elemszám = old elemszam –1 kifejezésben az old elemszam az elemszam változónak az eljárás lefutása előtti értékére hivatkozik. A teljes kifejezés azt jelenti, hogy az elem törlésével a verem elemszáma pontosan eggyel csökken.
Strip
Gyakran felmerül az igény olyan utófeltételek megfogalmazására, ahol több változó állapotának változatlanságát szeretnénk megfogalmazni. Ez természetesen kifejezhető az old szerkezettel. Azonban, ha egy eljárás majdnem összes változójára szeretnénk ilyen igényt megfogalmazni, akkor nem csak hosszú és nehezen áttekinthető kifejezéseket kapunk, és karbantartási nehézségekkel is kell szembesülnünk. A strip operátor nyújt megoldást ilyen esetben. A strip szintén csak utófeltételben használható. A strip utáni zárójelben egy attribútum listát lehet megadni. A strip operátor egy ARRAY[ANY] típusú tömböt határoz meg, ez a tömb azokat a globális változókat tartalmazza amelyek az osztályhoz tartoznak, de nem szerepelnek a zárójelben megadott attribútum listában. Ezzel olyan utófeltételeket fogalmazhatunk meg könnyedén, ahol az objektum bizonyos (néhány) változója megváltozik, míg a többi nem. A strip segítsége az, hogy pusztán azokat a változókat kell felsorolni, amelyek megváltoznak és nem azokat (általában ezekből van több) amelyek változatlanok. Például, ha az objektumban van egy tömb típusú attribútum, akkor megfogalmazhatjuk a következő állítást:
tomb ARRAY[G]
.
.
tobbi_valtozatlan: deep_equal(strip(tomb)), old strip(tomb))
A feltétel azt írja le, hogy az objektumban egyedül a tomb nevű tömb megváltozik – például egy rendezés eredményeként – de ezen kívül az objektum állapota változatlan marad.
Osztályinvariáns
Amikor egy osztályt tervezünk, egy jól meghatározott feladat érdekében tesszük, a feladat leírásában segít, ha olyan állításokat is megfogalmazhatunk, melyek mindig igazak egy osztály esetén. Akár azt is mondhatjuk, hogy ezek az logikai állítások – bizonyos szempontból – konzisztens állapotban tartják az osztályt. Az Eiffelben ezt az invariant kulcsszó alkalmazásával tehetjük meg. Az osztályinvariánsban megfogalmazott állításban osztály attribútumok és függvények közötti relációk is megfogalmazhatók. Az invariáns kifejezés onnan ered, hogy olyan feltételeket határoz meg, melyek az osztály példányainak életciklusa alatt minden kitüntetett időpillanatban a példányokon végzett műveletek során megőrzik igaz értéküket. Más szóval ezek olyan logikai kifejezések, melyek mindegyike True logikai értékkel rendelkezik és változásokra érzéketlen. Egy invariáns általában több logikai állításból áll össze, az osztályinvariánst képző logikai állítások az and then logikai operátorral vannak összekapcsolva a forráskódban meghatározott fizikai sorrend szerint. Természetesen, szigorúan véve egy osztály példány életciklusának minden pillanatában az invariáns nem lehet igaz, előfordulhatnak olyan állapotok – tipikusan feldolgozási vagy transzformációs lépések közben – amikor az invariáns nem teljesül. Ha jól meggondoljuk, akkor látjuk, ilyen esetekben nincs is szükség arra, hogy az invariáns teljesüljön. Ennek megfelelően az osztályinvariánsok kiértékelésre csak a nyilvános eljárások meghívása előtt és után (mint kitüntetett időpillanat) kerül sor.
Check
A programhelyesség-ellenőrzés talán egyik legegyszerűbb és legrégebben alkalmazott módszere, hogy a programfutás egy adott pontján megnézzük, hogy bizonyos általunk kívánatosnak tartott feltételek vajon fennállnak. Ezt sokszor if utasításokkal oldják meg, ha nem akarják a program futását félbeszakítani a feltétel nem teljesülése esetén. Más egyszerű eszköz is régóta rendelkezésre áll. Ilyen a C programozási nyelvben használt assert makró. Az assert-ben egy logikai feltételt adhatunk meg a C szintaktikai szabályok szerint, ha a feltétel igaz, nem történik semmi, ha a feltétel nem igaz, akkor futásidejű hiba keletkezik, a program megáll és kiírja, hogy melyik sorban nem teljesült a feltétel. Hasonló szerkezet az Eiffelben is megtalálható ez a check. A check utasítás után egy logikai feltételt kell írni. A check ellenőrzi, hogy az adott logikai feltétel vajon igaz az adott ponton. A check számos előnyt ad:
Ciklusok
A ciklusok helyes használata a programozás alapvető fontosságú része, ahol számos probléma felvetődhet.
Néhány gyakori probléma:
Ez az öt feltétel, amely a ciklus levezetési szabályában szerepel, ezeknek a feltételeknek kell fennállni, ha azt akarjuk, hogy egy ciklus helyesen működjön. Rövid magyarázat a feltételekhez:
from
inicializáló utasítások
until
kilépési feltétel
loop
ciklusmag
end
A variantés az invariant alkalmazása a cikluson belül a from és until közé ékelődik, használatuk opcionális.
Figyelem a check ciklusban is használható!
Íme egy példa:
-- egyszerű loop
simple_loop is
local
count: INTEGER
do
from
count := 1
invariant
count >= 1
count <= 201
variant
201 − count
until
count > 200
loop
io.put integer (count)
io.put new line
count := count + 1
end
end
Mikor helyes egy Eiffel ciklus? A ciklus akkor és csak akkor helyes, ha:
ahol:
INIT - ciklus inicializáló blokkja
BODY - ciklusmag
INV – ciklusinvariáns
EXIT – kilépési feltétel
VAR – termináló függvény
REQ – logikai kifejezés, milyen feltételek mellett hajtható végre a ciklus (előfeltétel)
v – egész típusú váltózó (a metódusban nem szerepel)
Összehasonlítva a bevprogos ciklus levezetési szabályokat és az Eiffel helyességi specifikációt – eltekintve a különböző formalizmustól – a következők állapíthatók meg: Először is az Eiffel ciklus feltétele más, mint a bevprogos. A bevprog szerint addig megy a ciklus, míg a ciklusfeltétel igaz, szemben az Eiffellel, ahol a ciklus addig megy amíg a ciklusfeltétel hamis. Ez a különbség, talán szintaktikai okokból jön, a bevprog while ciklusról beszél kimondatlanul, míg az Eiffelben az until kulcsszó után írjuk a feltétel. Más nyelvekből megszokva az until után olyan feltétel kell írni, ami ha igazzá válik, akkor a ciklus nem fut le többször.
Öröklődés
Az Eiffel lehetőséget a biztosít az öröklődés használatára az objektum-orientált programozás során. Az öröklődésnek két fontos aspektusa van, az implementáció öröklése és a típus öröklése. Az Eiffelben az öröklődési reláció egyúttal típusmegfelelőséget is definiál. Célszerű, tehát megvizsgálni az öröklődést típus-helyettesíthetőség és az elő- és utófeltételek szemszögéből. Röviden ismertetve a következő megállapítások adódnak: Ha egy C osztály B leszármazottja és c egy példánya C-nek, akkor c-nek használhatónak kell lenni minden olyan környezetben, ahol B osztály egy példánya is használható. Előfeltételek szempontjából ez csak akkor valósítható meg, ha C osztályban ugyanaz vagy egy gyengébb előfeltétel van használva. Az utófeltételeket tekintve, C osztályban ugyanazt vagy erősebb feltételt használva érthető el a helyes működés. Gyengébb feltételeket a meglévő feltételekhez, további feltételek logikai vagy művelettel történő összekapcsolása, míg erősebb feltételeket logikai és művelettel történő összekapcsolása ad. Öröklődés során lehetősége van metódusok átdefiniálására, az átdefiniált metódusok specifikációjában a require és az ensure kulcsszavak helyett rendre, require else és ensure else kulcsszavak használhatók. A metódusok teljes elő- és utófeltételei a következő módon alakulnak, ha az átdefiniálandó metódus előfeltétele E, utófeltétele U, az átdefiniált metódus előfeltétele E’, utófeltétele U’:
Osztály invariáns
Az öröklődés és az osztály invariáns kapcsolata egyszerűbb mint az öröklődés és az elő- és utófeltételek kapcsolata. Ennek oka, hogy az ősosztályok invariánsai algoritmikusan származtathatók, így nem szükséges minden osztályban az összes invariánst felsorolni. Elegendő csak azokat az invariánsokat megadni, amelyek bővítik az ősosztály invariánsait. Az osztályinvariánst kibővítve az ősosztályok invariánsaival együtt teljes osztályinvariánsnak nevezzük.
Az osztályinvariáns valamint az előfeltétel és utófeltétel kapcsolata
Felületes vizsgálódás alapján úgy tűnhet, hogy a sok feltétel közül az invariáns esetleg nem is szükséges. Mégis, az invariáns elkülönítése az elő- és utófeltételektől előnnyel jár:
Kivételkezelés és helyesség
Az Eiffelben a kivételkezelés helyessége elválik a programhelyesség-ellenőrzés kérdésétől.
A kivétel konzisztens egy publikus metódus akkor és csak akkor, ha a kivételkezelő blokk minden B ágára, ami nem retry utasítással ér véget,
{ True } B { I }, ami retry utasítással ér véget 
Hoare-formulák érvényesek.
Egy nem publikus metódus kivételkezelése akkor és csak akkor konzisztens, ha a kivételkezelő blokk minden B ágra, ami retry utasítással ér véget, { True } B { E } Hoare-formula érvényes. (Az I invariáns feltétel, az E előfeltétel ez eddigi jelöléseknek megfelelően.)
A kivételkezelő blokk minden ága a legszigorúbb True előfeltétellel rendelkezik. Ennek oka, hogy nem várt esemény után nem lehet támaszkodni, sem az előfeltételre, sem az invariánsra, hiszen a kivétel során a program abnormális állapotba kerülhetett.
Az alapvető programhelyesség-ellenőrzési nyelvi elemek és kapcsolataik ismeretében már meglehet vizsgálni, hogy áll össze az egész program helyessége.
Attribútumok helyessége
Minden attribútum helyesnek van feltételezve az alábbiak szerint:
Osztályok helyessége
Osztályok konzisztenciája
Az Eiffelben minden változó a típusától függő alapértelmezett értékkel rendelkezik. Egy osztály akkor és csak akkor konzisztens, egy I invariáns feltételre, ha mint teljes osztályinvariánsra bármely E előfeltételre és U utófeltételre nyilvános metódusra, ha a következő formulák érvényesek:
ahol:
D – az Eiffel változó típusától függő alapértelmezett értéke
B – az osztály törzse
A meghatározásban szereplő első feltételt akár tekinthetjük indukciós alaplépésnek, míg a második feltételt mint indukciós lépést. Ez utóbbi biztosítja, amennyiben az indukciós feltevés fennáll a művelet végrehajtása előtt, akkor konzisztens osztály esetén fenn fog állni a végrehajtás után is.
Osztályhelyesség
Egy osztály akkor és csak akkor helyes a specifikációra nézve (metódusok elő- és utófeltétele, teljes osztályinvariáns, check-konzisztens, helyes ciklus), ha konzisztens és minden metódusa helyes.
Programok helyessége
Egy Eiffel program, melynek futtatása egy osztály konstruktor metódusának meghívásával jár, akkor és csak akkor helyes a specifikációra nézve, ha az adott osztály helyes. Ezekből adódik, hogy a program akkor és csak akkor helyes, ha azok az osztályok, melyektől az adott osztály megvalósítása függ, mindegyike helyes.
A programhelyesség-ellenőrzés problémái
Függőségek
Az elv, hogy a program helyessége, a részek helyességétől függ, nem minden esetben alkalmazható közvetlenül. Az osztályok között többszörös függőségi viszony is fennállhat. A függőség tranzitív és szimmetrikus kapcsolat, ezen tulajdonságok folytán lehet olyan eset, amikor az osztályok helyességéről nem lehet külön-külön megállapítást tenni, csak is együttesen.
Helyességi specifikációs nyelv
A helyességi-specifikációs nyelv ismertetése során hangsúlyt kapott, hogy az egzisztenciális és univerzális kvantor nem használható ezekben a logikai kifejezésekben. Azonban megfelelő függvények felhasználásával helyettesítésük megoldható. Nyilvánvalóan ilyen esetben, az alkalmazott függvény helyességét is biztosítani kell. Algoritmusok végrehajtása azonban ellentétben van a specifikációs nyelv deklaratív formájával. Így csak körültekintően alkalmazhatók a függvények a kvantorok kiváltására.
Elméleti korlát
Az axiomatikus szemantika – ahogy a feltételeket megadjuk – kifejező ereje gyengébb az un. operációs szemantikánál vagyis, ha még lenne is egy ideális specifikációs nyelv, akkor sem lenne megfogalmazható állításokkal a program működésének minden lényeges aspektusa.