Boolean Expression
5.1 Állapotalapú specifikációk
Az állapotalapú specifikációk a szoftverrendszereket állapotok és az állapotokon végzett műveletek hatásai szempontjából írják le. Az ilyen specifikációkat számos specifikációs nyelv támogatja, amelyeket két csoportba soroltunk: a klasszikus specifikációs nyelvek, mint a Z , a B és a VDM , és az állításnyelvek, mint az Eiffel , a JML (Java Modeling Language) , valamint Peters és Parnas táblázatai . Míg a klasszikus specifikációs nyelvek a megvalósítástól függetlenül határozzák meg az állapotokat és az átmeneteket, addig az állítási nyelvek a forrásprogram utasításai vagy megjegyzései formájában határozzák meg az állapotokat és az átmeneteket.
Az állapotalapú specifikációkat tesztorákulumokként használják azáltal, hogy ellenőrzik a tesztvégrehajtások specifikációknak való megfelelését. Az állapotalapú specifikációkból történő tesztorakelek előállításának fő problémája a specifikációk és a tesztvégrehajtás során ellenőrzött műveletek közötti eltérő absztrakciós szintekből adódik; így a műveletek specifikációit ellenőrizhető formába kell fordítani. A specifikációs nyelvek általában elég kifejezőek a különböző adatszerkezetek és állapotalapú tulajdonságok ábrázolásához, de kifejezőerejük megnehezíti a futtatható formába való fordítást. A fordítás gyakran tesz néhány egyszerűsítő feltételezést, például korlátozza a végtelen halmazokat, például a természetes számok végtelen halmazát, és a nem végrehajtható elemeket csak részben kezeli, és néha emberi beavatkozást igényel.
A következőkben az állapotalapú specifikációk végrehajtható formába történő fordításának főbb megközelítéseit tárgyaljuk. A Z, B és VDM specifikációk fordítása ugyanolyan problémákat vet fel, mint a végtelen adatstruktúrák, a részlegesen definiált kifejezések és az objektumorientált struktúrák. Az Eiffel, a JML és más állításnyelvek lefordítása ellenőrizhető formába hasonló problémákat vet fel, de más absztrakciós szinten. A következőkben bemutatjuk az állapotalapú specifikációk Z-re hivatkozva ellenőrizhető formába történő fordításának főbb megközelítéseit; más nyelvek esetében a megközelítések hasonlóak. Ezután az állítások végrehajtható ellenőrizhetővé fordításának problémáit tárgyaljuk az Eiffelre, a JML-re, valamint Peters és Parnas táblázataira hivatkozva.
A Mikk által javasolt séma predikátum fordító a Z specifikációkat C kódba fordítja. A megközelítés minden egyes Z sémához, amely a Z alapegysége, egy C függvényt generál, amely a séma predikátumokat a függvénynek paraméterként átadott programállapot felhasználásával értékeli ki. A generált kód a séma predikátumait “nyers erő” stratégiával értékeli ki: Adott állapot esetén a kód lényegében kicseréli a kifejezéseket azok értékeire, az igazságtáblák segítségével kiértékeli a tételes számítási formulákat, és az adatstruktúrák iterálásával kiértékeli a kvantifikációkat és a halmazkonstrukciókat. A generált C függvények komplexitásának csökkentése érdekében a megközelítés egy optimalizálási lépést javasol annak biztosítására, hogy a generált C kód mindig befejeződjön. A kód optimalizálásához a technika meghatározza a Z nyelv egy “végrehajtható” részhalmazát. Az alhalmaz véges predikátumokból áll, például kijelentésszámítási formulákból, véges halmazok feletti kvantifikációkból és véges iteráción alapuló halmazkonstrukciókból. A technika a végrehajtható predikátumok halmazát egy olyan szabálykészlettel bővíti, amely bizonyos feltételeknek megfelelő speciális, nem végrehajtható predikátumokat szemantikájuk megváltoztatása nélkül alakít át végrehajthatóvá. Például a következő két szabály kiküszöböli a kvantorokat:
ahol M egy halmaz, az x változó M egy elemét jelenti, P pedig egy predikátum. A – operátor, más néven a “Z jelölés foltja” a ∃ kvantorral együtt használva azt jelenti, hogy “olyan, hogy”, a ∀ kvantorral együtt használva pedig azt, hogy “hogy”. Például ∃ x : M – P azt jelenti, hogy létezik legalább egy olyan x érték M-ben, hogy a P predikátum igaz. A NotOccur(x, P) feltétel azt jelzi, hogy x nem szabad változó a P predikátumban. Bár az M halmaz lehet végtelen, a fordító mégis képes az M feletti kvantorokat használó specifikációk összeállítására, amennyiben a kvantorok a fenti szabályok alkalmazásával kiküszöbölhetők. A felhasználó által definiált függvények esetében, amelyeket axiomatikus vagy általános definíciókkal lehet bevezetni, a fordító megköveteli, hogy a felhasználó adja meg a megfelelő kódot. A Mikk megoldást javasol a részlegesen definiált specifikációk problémájára is. Ő a VDM-SL-t, mint köztes formát és a Schmidt és Hörcher által kifejlesztett VDM-SL fordítót használja a Z specifikációk C kódra történő lefordítására . Amikor részlegesen definiált kifejezéseket kezel, azaz függvényeket vagy relációkat, amelyek definiálatlanul (⊥-val jelölve) értékelhetők, ha a definíciós tartományukon kívül értékelik ki őket, a megközelítés kivételkezelőket generál.
A Z objektumorientált kiterjesztései, mint például az Object-Z, súlyosbítják a problémákat. McDonald et al. a konténerosztályok Ojbect-Z specifikációit három lépésben fordítják le C++ kódra: optimalizálás, strukturális leképezés és predikátumfordítás . Az optimalizálási szakaszban több lépésben átrendezik a specifikációt, hogy egyszerűsítsék a későbbi fordítást, beleértve a konstans változók értékekkel való helyettesítését, valamint a másodlagos változók és a sémadúsítások eltávolítását. A strukturális leképezés szakaszában az Object-Z specifikációban szereplő struktúrákat képezik le a megfelelő kódelemekre: A specifikációs konstansokat és változókat megfelelő inicializálású változókra, a változók típusait pedig primitív C++ típusokra vagy a technika által használt Z eszköztár könyvtárának megfelelő osztályaira. Például az integer és boolean típusokat int-re, az integer halmazok típusát pedig z_set<int >-re képezik le. Az inicializálási sémát konstruktorra, a műveleti sémákat pedig tagfüggvényekre képezik le, létrehoznak egy speciális tagfüggvényt, az inv()-t az osztály invariánsának ellenőrzésére, és minden egyes kivételsémához létrehoznak egy kivételosztályt.
A predikátum DeepL fordításban a technika arra összpontosít, hogy a predikátumok kiértékelése helyett hogyan generáljuk a programállapot ellenőrzésére szolgáló kódot. A fordítás például megakadályozza, hogy az inv() függvény bármely más tagfüggvényt meghívjon, a végtelen rekurzió elkerülése érdekében. Egy konstruktorban az osztály invariánsát a kilépéskor ellenőrzik.
Richardson et al. az időkritikus rendszerekre koncentrál, a Z és az időintervallum logika kombinációjával foglalkozik, és a specifikációk tesztorákulumokká való fordítását javasolja szimbolikus értelmezéssel. A szimbolikus értelmezés a specifikációkban szereplő szimbolikus neveket az adat- és vezérlési leképezésekre hivatkozva hozzárendeli az ingerbemenetekhez és a kezdeti állapotváltozókhoz. Ezután a szimbolikus értelmezés értelmezi a specifikációk minden egyes vezérlési útvonalát, azaz létrehoz egy állítást, amely a specifikáció adatainak feltételét fejezi ki az egyes specifikációs vezérlési pontok szimbolikus állapota alapján. Egy specifikációs ellenőrzési pont egy releváns elem, például egy paraméterezett esemény, egy átmenet és egy művelet. A Z specifikáció szimbolikus értelmezése után az orákuluminformáció a releváns Z sémák és a hozzájuk tartozó állítások listájaként jelenik meg, amelyeket a séma meghívása esetén ellenőrizni kell. Egy teszteset végrehajtása egy konkrét tesztbemenetre utal, amelyből konkrét változókat és eseményeket kötünk a tesztosztályban lévő megfelelőikhez (minden tesztosztály a tesztbemenet egy partíciója). A teszteset végrehajtása egy végrehajtási profilt eredményez, és a végrehajtási profilban szereplő konkrét eseményeket és változók értékeit leképezzük az orákulum szintjére, hogy ellenőrizzük a konzisztenciájukat az orákulum információival.
Az asszertív nyelvek egyesítik a specifikációkat a forráskóddal, így egyszerűsítik, de nem szüntetik meg a fordítási problémát. Az állítmányokat különböző nyelvek és módszertanok támogatják. A szerződéses tervezés egy olyan szoftvertervezési paradigma, amely a kód és az állítások közös tervezését tételezi fel. A szerződéses tervezést Meyer javasolta, és az Eiffel programozási nyelv teljes mértékben támogatja. Az olyan általános specifikációs nyelvektől eltérően, mint a Z, az Eiffelben a szerződéseknek nevezett specifikációkat a forráskódba olvasztják, és jól megtervezett interfészeken keresztül kommunikáló szoftverkomponensek kötelezettségeit és előnyeit határozzák meg. A szerződéseket támogató nyelvekben az ügyfél kötelezettségei és előnyei a szolgáltatók elő- és utófeltételeiként vannak kifejezve. A forráskódot olyan invariánsokkal gazdagítják, amelyek olyan állapottulajdonságokat képviselnek, amelyeknek minden interakció során fenn kell állniuk.
A szerződéseket számos nyelvre kiterjesztették. Az iContract volt az első eszköz, amely támogatta a szerződéseket Java nyelven. Az iContract-ban a szerződések speciális címkékkel ellátott kódkommentárként íródnak. Az iContract által támogatott szerződések a Java szintaxisának megfelelő bólés kifejezések, kivéve néhány szintaktikai kiterjesztést, amelyek közé tartozik az univerzális kvantifikáció (∀), az egzisztenciális kvantifikáció (∃) és az implikáció (→). Ezek a kiterjesztések a Java kódba való lefordításuk egyszerűsítését szolgálják. Például, the syntax of ∀ is forall < Class >< var > in < Enum >< Exp_var >, where < Class > is the type of the variable < var >, which represents an element of < Enum >. A reasonable translation of the ∀ expression is to use a Java loop to iterate over the enumeration < Enum > and evaluate the boolean expression < Exp_var > in each iteration. The existential quantification is translated similarly. An implication expression C implies I can be simply translated into an if statement: “if C then check I.”
A bólés kifejezések egyszerű fordításán kívül az iContract foglalkozik az objektum életciklusával, a változók hatókörével és az örökléssel kapcsolatos kérdésekkel, amelyek többsége az objektumorientált programozás sajátja. Az objektum életciklusával kapcsolatos legfontosabb szabályok a következők:
Az objektum felépítésénél az előfeltételeket a felépítés kezdetén kell ellenőrizni, míg az invariánsokat és a posztfeltételeket csak akkor, ha a felépítés normálisan (kivételek nélkül) befejeződik.
Az objektumok normál metódushívásainál az elő- és utófeltételeket a meghívott metódusok belépésekor és kilépéskor kell ellenőrizni, a privát metódusoknál pedig az invariánsokat nem kell ellenőrizni.
Az objektumok megsemmisítésénél nincs szükség ellenőrzésre. Így a finalize() metódusokba nem kerül be ellenőrző kód.
A posztfeltételekben használt predikátumok gyakran hivatkoznak mind a metódus visszatérési értékére, mind egyes változók “régi” értékére (vagy “belépési értékére”). Az iContract szintetizál egy return nevű pszeudováltozót a visszatérési érték reprezentálására, a változó értékeit a belépési értéknél tárolja, és a változók neveként a @pre utótaggal teszi elérhetővé. kifejezések, objektumhivatkozásaikat közvetlenül tárolja. iContract lehetővé teszi a tagmetódusok hívását a szerződésekben. Ennek eredményeként az invariánsok ellenőrzése során potenciálisan végtelen rekurzió léphet fel. Ennek a problémának a megoldására az iContract minden szálon belül nyomon követi az egyes objektumok rekurziós mélységét, és csak a 0 mélységű invariánsokat ellenőrzi. A Java típusbővítési mechanizmusai számos hatással vannak arra, hogyan kell kezelni a típusok szerződéseit. Az iContract a következő szabályok szerint szaporítja a szerződéseket:
Az invariánsok konjunkcióban vannak, azaz egy altípus invariánsa az összes szupertípusának invariánsainak konjunkciója.
Az utófeltételek konjunkcióban vannak, azaz egy altípus utófeltétele az összes szupertípusa utófeltételeinek konjunkciója.
A előfeltételek diszjunkcióban vannak, azaz egy altípus előfeltétele az összes szupertípusa előfeltételeinek diszjunkciója.
A JML egy népszerű viselkedéses specifikációs nyelv, amely támogatja a Design by Contract Java . A JML szerződések a Java-ban speciális megjegyzések formájában jelennek meg. A JML az előfeltételeket, utófeltételeket és invariánsokat boolean kifejezésekként fejezi ki, amelyeket a requires, ensures és invariant kulcsszavak előznek meg, és beépített \ old(x) metódust használ az x értékének egy művelet előtti ábrázolására. A Z-ben használt ▵ jelöléshez hasonlóan a JML a modifies kulcsszóval jelzi a metódus testében megváltozott változókat. A JML továbbá számos objektumorientált jellemzővel foglalkozik, például a láthatósággal és az örökléssel.
A JML a tesztorákulum-generálás számos megközelítésének alapja. Bhorkar javasolt egy technikát a JML szerződések Java állításokká történő lefordítására . Bár csak előfeltételeket támogat, ez a technika foglalkozik a csak specifikációs változókkal, a finomítással, a specifikációs örökléssel és az adatvédelemmel kapcsolatos kérdésekkel. Az iContract-hoz hasonlóan a technika a szerződések öröklését úgy kezeli, hogy a szerződéseket a típusuknak megfelelően konjunktív és diszjunktív módon kapcsolja össze és szét. A technika egy hash-táblázatot is használ (szálanként) a rekurziók elkerülése érdekében a futásidejű ellenőrzés során. A kvantorokat használó kifejezéseket a technika nem végrehajthatónak tekinti, és az ilyen kifejezésekhez nem generál Java kódot.
Korat egy olyan technikát javasolt, amellyel a JML specifikációkból teszteseteket és orákulumokat lehet generálni. Korat technikája teszteseteket generál előfeltételekből és invariánsokból, és orákulumokat posztfeltételekből és invariánsokból. Araujo et al. kibővítette a JML-t egyidejű szerződésekkel, és futásidejű támogatást javasolt az egyidejű tulajdonságokat specifikáló állítások futásidejű ellenőrzésének lehetővé tételére .
Peters és Parnas bevezetett egy megközelítést a formális dokumentációból történő tesztorákulumok generálására . A dokumentációt táblázatos formában adják meg, amely az eljárások interfészeit specifikáló relációkból áll, és C és C++ kódú orákulumokba fordítják le. A formális dokumentáció központi eleme a predikátumlogika egy olyan változatában írt predikátumkifejezésekből áll, amely speciális konstrukciókat tartalmaz a részleges függvények kezelésére. Más specifikáció-alapú orákulumtechnikákhoz hasonlóan ez a technika a kvantorokat úgy kezeli, hogy véges halmazokra korlátozza őket.
Azért, hogy lehetővé tegye a kvantorokat tartalmazó elemhalmazokon való iterációt, Peters és Parnas induktívan definiált predikátumokat vezet be. Egy (kvantorokban használandó) S halmazhoz egy induktívan definiált P predikátumot definiálnak három elemmel: I, G és Q. Az I kezdeti halmaz véges számú elemet tartalmaz, G egy “generátorfüggvénynek” nevezett függvény, amely a halmaz elemeit generálja, Q pedig egy predikátum, amely a halmaz tulajdonságait jellemzi. Az S halmaz az alábbi induktív lépésekkel konstruált legkisebb halmazként definiálható:
S0 = I
Sn + 1 = Sn ∪ {G(x)|x ∈ Sn ∧ Q(x)}
I, G és Q úgy kell definiálni, hogy megfeleljenek egy speciális feltételnek, amely biztosítja, hogy a konstruált S halmaz véges legyen.
Peters és Parnas egy megközelítést javasol a táblázatos dokumentációk C kódra fordítására. Mivel a dokumentációkban használt kifejezések formája jól definiált, a fordítás szisztematikusan történik.
A tesztorákulumok levezetéséhez más állapotalapú specifikációkat is használnak. Az UML-modellek általában informálisak; ennek ellenére Bouquet et al. definiálta az UML 2.1 egy részhalmazát, az UML-MBT-t, amely elég pontos a tesztesetek automatikus generálásához. Az UML-MBT osztálydiagramokat, állapotgépeket és az OCL 2.0 egy részhalmazát tartalmazza. Bouquet et al. a VDM-SL nyelven írt specifikációkat használja a tesztorákulumok generálásához.