0. A módszer matematikai modellje
Ebben a részben a módszer teljesítőképességét vesszük górcső alá. Megvizsgáljuk a működésének elméleti alapjait, és alkalmazásának gyakorlatát.
Az elméleti taglaláshoz néhány alapfogalomra lesz szükségünk. Nagyban építünk a [KV2001] irodalomra, így jónéhány fogalmat definiálás nélkül átveszünk. (Pl. típusosztályhoz kapcsolódó szignatúra, specifikáció absztrakt fogalmait.)
|
|
Definíció – P/P-specifikáció Egy TIP
tipusosztály P/P-specifikációja alatt a P/P-specTIP={S,EPP},
ahol S=(S,OP)
szignatúra és EPP={(Efi ,Ufi)
i=1..║OP║} (Efi ,Ufi) elő- és
utófeltételek véges halmazát értjük, ║OP║ a TIP
operációinak a számát jelenti. |
Értelemszerűen az (Efi
,Ufi) elő- és utófeltétel-pár a TIP i. operációjához tartozik.
(Arról azonban tudjunk, hogy minden operáció előfeltétele az implicit
error-axiómával együtt ki kell, adja a bemeneti értékek összességét. Azaz
valójában nincs az operáció használata korlátozva, de lényegi transzformációra
csak a fenti előfeltételek teljesülése mellett számíthatunk. Tegyük ehhez hozzá
azt, hogy ha az operátor NemDef
értéket állít elő, akkor a bemeneti értékeket változatlan értékben meghagyja.)
Példul:
|
|
Definíció – algebrai specifikáció Egy TIP
tipusosztály algebrai specifikációja alatt a Alg-specTIP={S,Eax},
ahol S=(S,OP)
szignatúra és Eax={Axi i=1..N} Axi axiómák
véges halmazát értjük. Az axióma egy
leképezés a típus bázishalmazáról (T0) a logikai értékek (L) halmazára: Ax: T0 ® L |
Az axiómák tartalmazzák a TIP-hoz rendelt operációk közül számosat. Ezek kapcsolatait írják le. Vizsgálatunk tárgya, hogy az operációk működését leíró P/P-specifikációk jól illenek-e bele az axiómák rendszerébe. Értelmes felvetés tehát egy axióma igazságtartalmára rákérdezni. Vagyis egy adott bázishalmazbeli értékből kiindulva az egyes axiómák igazak-e, amint „megszólaltatják” és kapcsolatba hozzák egymással a bennük foglalt műveleteket.
Példul:
L. sor algebrai specifikációját!
|
|
Definíció – Operátor P/P-kiértékelése Adott egy TIP
tipusosztály P/P-specTIP={S,EPP} P/P-specifikációja.
Az (Efi ,Ufi) ÎEpp elő-
utófeltétellel adott operációjának tÎT0 melletti
P/P-kiért(op,t) kiértékelése alatt azon értékek halmazát
értjük (ÍRop), amelyet úgy
kapunk, hogy bármely, az előfeltételt teljesítő paraméterezése és az adott t
mellett az operátor kimeneti értékei az utófeltételt kielégítik. Azaz ha op:T0xTi1x…xTij®T0xTikx…xTim,
A {(t1,…,tj)ÎTi1x…xTij:
Efop(t, t1,…,tj)} halmazt nevezzük az operátor t melletti tartójának. S
jelöljük így: Tartó(op,t), |
(tt, tt1,…,ttm)=op(t, t1,…,tj), azaz (tt, tt1,…,ttm) jelöli az operátor által transzformált értéket a (t, t1,…,tj) helyen; továbbá a Ti1x…xTij halmaz a paramétereinek a halmaza. A tartó tehát azon halmaz, amelybe tartozó paraméterek estén elvárható az operátor utófeltétel szerinti működése.
Például:
A sor bázishalmazát jelöljük S-sel, ami Elem-iterált – amint ez az exportmodul nyitó részéből derül ki. A Sorból és az Üres? operációk szignatúrája az algebrai specifikációban szereplőtől némileg eltér. Pontosítottuk az exportmodulban olvashatók szerint: hozzávettük a definiáltság-állapotát jelző {Def, NemDef} komponenst „hiba” néven. Ezt mint latens paramétert tekintjük; azaz a sor belső komponenseként használjuk, az operátorok paraméterei között explicite nem, csak a sor részeként fog megjelenni. Emiatt az axiómákat újrafogalmazni kényszerülünk.
Sorból: Sor x hiba ® Sor x hiba x Elem [2]
Üres?: Sor x hiba ® Sor
x hiba x L
ahol
hiba={Def,NemDef}
L={Igaz,Hamis}
Exportmodulbeli P/P-specifikációik:
Eljárás
Sorból(Változó s:Sor,
e:ElemTip)
[a
sor első elemének kivétele]
Ef: $sÎSor Ù
Øs.hiba
Uf: s.sorozat=(s1,...,sn)
Þ
s’=((s2,...,sn),Hamis) Ù e=s1
s=() Þ s’.hiba=Igaz
Függvény
Üres?(Konstans
s:Sor): Logikai
[üres-e
a Sor]
Ef: $sÎSor Ù
Øs.hiba
Uf: Üres?(s)=(s.sorozat=())
Lássunk néhány P/P-kiértékelést:
1. mintastruktúra a Sorból operációhoz: ( ) – üres sorozat
a) Tartó(Sorból, ( )):={Def}
ui.: EfSorból(( ), Def)=Igaz, EfSorból(( ), NemDef)=Hamis Þ Tartó(Sorból, ( )):={Def}
(azaz csak a Def paraméterre
teljesül az előfeltétel, 1-elemű a tartó az üres sorozatra)
b) P/P-kiért(Sorból, ( )):={(( ),NemDef,e) : "eÎElem }
ui.: "hÎTartó(Sorból, ( )), a)Þ $!h=Def
(szavakkal:
az üres sorozat mellett, elegendő csak a Def-re meghatározni azt a kimeneti
halmazt, amelyre az utófeltétel igaz)
UfSorból((ss,hh,ee), (( ),Def))=Igaz Û ss=( ) Ù hh=NemDef Ù ee=e "eÎElem
(szavakkal: az utófeltétel igaz
lesz NemDef állapot és üres sorozat mellett tetszőleges elemre).
2. mintastruktúra a Sorból operációhoz: (e) – egy elemű sorozat
a) Tartó(Sorból, (e)):={Def}
ui.: EfSorból(((e), Def))=Igaz, EfSorból((e), NemDef)=Hamis Þ Tartó(Sorból, (e)):={Def}
b) P/P-kiért(Sorból, (e)):={(( ),Def,e)}
ui.: "hÎTartó(Sorból, (e)), a)Þ $!h=Def
UfSorból((ss,hh,ee), ((e),Def))=Igaz Û ss=( ) Ù hh=Def Ù ee=e;
3. mintastruktúra az Üres? operációhoz: ( ) – üres sorozat
a) Tartó(Üres?, ( )):={Def}
ui.: EfÜres?((( ), Def))=Igaz, EfÜres?((( ), NemDef))=Hamis Þ Tartó(Üres?, ( )):={Def}
b) P/P-kiért(Üres?, ( )):={(( ),Def,Igaz)}
ui.: "hÎTartó(Üres?,( )), a)Þ $!h=Def
UfÜres?((ss,hh,ll), (( ),Def))=Igaz Û ss=( ) Ù hh=Def Ù ll=Igaz;
4. mintastruktúra az Üres? operációhoz: (e) – egy elemű sorozat
a) Tartó(Üres?, (e)):={Def}
ui.: EfÜres?(((e),Def))=Igaz, EfÜres?(((e), NemDef))=Hamis Þ Tartó(Üres?, (e)):={Def}
b) P/P-kiért(Üres?, (e)):={((e),Def,Hamis)}
ui.: "hÎTartó(Üres?, (e)), a)Þ $!h=Def
UfÜres?((ss,hh,ll), ((e),Def))=Igaz Û ss=(e) Ù hh=Def Ù ll=Hamis;
5. … egy nem ennyire triviális példa
…
|
|
Definíció – Axióma
kiértékelése Adott egy TIP tipusosztály Alg-specTIP={S,Eax}
algebrai specifikációja és P/P-specTIP={S,EPP}
P/P-specifikációja. Az AxÎEax axiómájának tÎT0
melletti Ax-kiért(Ax,t) kiértékelése alatt azon logikai érték a.) a
logikai műveletek kiértékelési sorrendjének megfelelően sorbavesszük az
operátorokat, abból a célból, hogy b.) külön-külön
kiértékeljük; természetesen az elsőt az adott t-re, a továbbiakat olyan
paraméterekre, amelyeket az addigi kiértékelések meghatároznak; c.) majd
figyelembe vesszük az előírt logikai műveleteket, megkapjuk a végeredményt. |
Például:
Az eredeti 4’o axióma:
4’o Sorból – hiba-axióma
Üres?(s) Þ Sorból(s)=NemDef
… és az újrafogalmazott változata:
4’o Sorból – hiba-axióma
Üres?(s).L Þ Sorból(s).hiba=NemDef
1. mintastruktúra a 4’o axiómához: ( ) – üres sorozat
Ax-kiért(4’ o, ( )) º …
a) A kiértékelés sorrendje és a művelet paramétere:
- Üres? – ( )
- Sorból – P/P-kiért(Üres?, ( )) meghatározta Sor-komponens
b) A korábbi példákat alapul véve:
P/P-kiért(Üres?, ( )):={(( ),Def,Igaz)},
Ennek Sor-komponense: ( ), ezért
P/P-kiért(Sorból, ( )):={(( ),NemDef,e) : "eÎElem }.
Így
Ax-kiért(4’ o, ( )) º
º Üres?((( ),Def)).L Þ
Sorból((( ),Def)).hiba=NemDef º
º Igaz Þ
NemDef=NemDef º
º Igaz
2. mintastruktúra a 4’o axiómához: (e) – egy elemű sorozat
Ax-kiért(4’ o,((e),Def)) º …
a) A kiértékelés sorrendje és a művelet paramétere:
- Üres? – (e)
- Sorból – P/P-kiért(Üres?, (e)) meghatározta Sor-komponens
b) A korábbi példákat alapul véve:
P/P-kiért(Üres?, (e)):={((e),Def,Hamis)},
Ennek Sor-komponense: (e), ezért
P/P-kiért(Sorból, (e)):={(( ),Def,e)}.
Így
Ax-kiért(4’ o,((e),Def)) º
º Üres?(((e),Def)).L Þ
Sorból(((e),Def)).hiba=NemDef º
º Hamis Þ
((),Def)=NemDef º
º Igaz
|
|
Definíció – mintastruktúrák halmazának
Ax-szerinti partícionálása Adott
egy TIP tipusosztály P/P-specTIP={S, EPP}
P/P-specifikációja és az Alg-specTIP={S, Eax} algebrai
specifikációja. A t1,t2ÎT0
ugyanabba T0–partícióba tartozik egy adott AxÎEax
szerint, Jelöljük egy tÎT0-t
tartalmazó partíciót: Partíció(P/P-specTIP,Ax-specTIP,Ax,t); |
Így elegendő mindig csak a partíció valamely reprezentánsát vizsgálni. Értelmes általánosítása ezeknek, a minden axiómát figyelembe vevő partícionálás és reprezentánsok halmaza.
Például:
t1=((
),Def), t2=((e),Def), t1,t2ÎT0:
t1¹t2
(előző példák) Þ
Ax-kiért(4’o,t1)=Ax-kiért(4’o,(( ),Def))=Igaz Ù
Ax-kiért(4’o,t2)=Ax-kiért(4’o,((e),Def))=Igaz
Þ
Partíció(P/P-specTIP,Ax-specTIP,Ax,t1)=Partíció(P/P-specTIP,Ax-specTIP,Ax,t2).
|
|
Definíció – P/P-specifikáció kompatibilitása az
Ax axiómával Egy
TIP tipusosztály P/P-specTIP={S,EPP} P/P-specifikációja
kompatíbilis az Alg-specTIP={S, Eax} algebrai
specifikáció egy AxÎEax axiómájával, ha "tÎReprezentáns(P/P-specTIP,Ax-specTIP,Ax)
mintastruktúra esetén Ax kiértékelése igaz értékre vezet. |
Például:
|
|
Definíció – P/P-specifikáció kompatibilitása az
algebrai specifikációval Egy
TIP tipusosztály P/P-specTIP={S,EPP} P/P-specifikációja
kompatíbilis az Alg-specTIP={S, Eax} algebrai
specifikációjával, ha "tÎReprezentáns(P/P-specTIP,Ax-specTIP)
mintastruktúra esetén minden axióma kiértékelése igaz értékre vezet. |
Például:
1. A megbízhatóság
1.1. A megbízhatóság fogalma
A megbízhatóságon két dolgot értünk: egyrészt, ha a program elfogad egy axiómát jónak, akkor mennyire hihetünk eben; másrészt ha hibásnak jelez egy axiómát, akkor az valóban inkompatibilitást jelez-e?
Az első részéhez keserű tapasztalatok fűződnek. Vannak „szerencsétlen interferencia” okozta kimutatlanul maradt hibák. Lássunk ezek közül néhányat!
1.2. Rejtett hibák
A verem példánál maradva, könnyű olyan hibás P/P-szabályt találni az Üres és az ÜresE operátorhoz, amelyek menthetetlenül elfedik egymás hibáját. [Verst3H1]
|
a hibás
operációk szabályai[3] |
axióma |
Prolog „lényegi” szabály[4] |
|
ures(verem([],nemDef)). uresE(verem(_,nemDef),_). |
1º Üres – axióma V=Üres Û Üres?(V) |
axioma1(V,igaz) if |
A verem([],def) paraméterrel hívva az axioma1 szabályt, az ures(V) illeszthetetlen volta miatt rögvest fail-lel visszalép, és a 2. alternatívára tér át. Itt a not(ures(V)) true lesz, de nem várt ok miatt: nem az ürességet, hanem a definiáltságot kifogásolja a Prolog. Továbblépve a not(uresE(V,igaz)) a hibás uresE axióma miatt lesz true. A végeredmény: az axioma1 teljesül!
A verem([],nemDef) paraméterrel aktivizálva az axioma1-et azon csúszik el a hibaérzékelés, hogy a hibás Üres szabályon áthalad a vezérlés az ÜresE helyesen megfogalmazott implicit-error axióma miatt tényleges vizsgálódás nélkül jut túl.
Egy másik példában a Tető és a Verembe operációk interferálnak rosszul. [VerSt3H2]
|
a hibás
operációk szabályai |
axióma |
Prolog „lényegi” szabály |
|
teto(verem(V,nemDef),_, verembe(verem(V,nemDef),_, |
3º Tető-Verembe – axióma Tető(Verembe |
axioma3(V,igaz)if |
A verem([],def) paraméterrel hívva az axioma3 szabályt, minden joggal rendben fut le. A verem([],nemDef)-re viszont a válasz hibásan lesz igenlő. Ui.: a verembe(V,E,W) úgy tud illesztődni a hibás az implicit-error axiómához, hogy közben a Tető hasonlóan hibás axiómája együttesen is elfogadhatóvá teszi az axiómát.
Az „abszolút” megbízhatóság elvileg sem biztosítható. Ezt mondja ki az alábbi állítás.
|
|
Állítás: Ha a típus axiómái között található alábbi (*) szerkezetű,
akkor a benne szereplő operációknak van olyan átértelmezése –szemantikus
módosítása–, amelyre az axióma változatlanul igaz marad. (*) opk,
opsÎOP, ops:T0®TiÈ{NemDef}, opk:®T0È{NemDef}, AÎTi, Bizonyítás: Könnyen definiálható olyan ops’:
T0®TiÈ{NemDef}, opk’:®T0È{NemDef}, amelyre Konstrukció:
Az operációkat P/P-specifikációval adjuk meg. Tehát: P/P-spec(opk):
Legyenek a módosított operátorok az alábbi módon definiálva: P/P-spec(opk’):
|
Megjegyzem: a bizonyítás nyilvánvalóságot formalizál. Nem állítom, hogy a hibák képződésének „gyakorlatias” módját mintázza. Cél csak annyi volt, hogy beláttassa: rejtve maradó hibák létezhetnek.
Az állítás után mire számíthatunk a módszer használhatóságát illetően?
Szerencsére ritka az olyan abszolút szerencsétlen interferencia, amely teljesen rejtve tud maradni. Ezt példázza a [Verst3H1] program is, amelyben ugyan az 1o axiómában szereplő két hibás operáció el tudott rejtőzni, de a 4o axiómában egy hiba mégis felszínre került. Ez alapján már gyanú ébredhet az ÜresE operációval szemben. Azt javítva, már az 1o axióma is jelzi a „maradék” problémát. L. az 1.1. és 1.2. ábrát!
Hasonlóan tárulkozik fel az elfedődött hiba [VerSt3H2] program példájában. Kezdetben a három hiba 2 axiómában jelződik, de a 3o és a 3’o axiómában rejtve maradnak a hibás operátorok. L. az 1.3. és 1.4. ábrát! A hibajelzés után a gyanús ÜresE operációról bebizonyosodott a helytelen specifikáció, amit javítunk. A javítás után újabb hibajelzés, újabb javítás… A dolog érdekessége az, hogy a hibák javítása közben soha sem jutottunk olyan időleges állapotba, amely során az elemzett 3o axióma hibásnak mutatkozott volna. Ez nem is probléma, hisz a lényeg, hogy amíg hiba volt, addig volt hibásnak talált axióma is.
|
1.1.
ábra – futási eredmény |
|
|
|
1.2.
ábra – futási eredmény |
|
1.3.
ábra – futási eredmény |
|
|
|
1.4.
ábra – futási eredmény |
Megállapíthatjuk, hogy a hibák rejtve maradása ellen úgy védekezhetünk, hogy minél inkább „redundánssá” tesszük az algebrai rendszert. Ennek egy kitűnő eszköze lehet a típusosztályt jellemző állítások kimondása, formalizálása, és a Prolog programba való beillesztése.
Amint már korábban hangsúlyoztuk, a hibák rejtve maradásának másik oka az lehet, ha nem megfelelően választjuk meg a típusosztályt tesztelő mintastruktúrákat. Itt vezérelvként jelentettük ki: egy sorozattípus esetén minden közvetlenül hivatkozott elemnek legalább egy mintastruktúrában fel kell bukkannia. Más szóval, ha van opi operátor, amely a sorozat i. elemével tesz valamit (módosítja, beszúr elé/mögé, törli, vagy egyszerűen az értékét teszteli), kell legalább egy legalább i db elemet tartalmazó mintasorozat.
1.3. Hamis riasztás
A módszer lényegéből fakadóan, feltéve a P/P- és az algebrai specifikáció precíz kódolását, csak olyan axiómák esetében jelez „fölöslegesen” inkompatibilitást, ha az axióma nem fedi le a „teljes esemény rendszert”. Vagyis hiányzik olyan alternatíva, amely nem képes „elfogadólag nyilatkozni” valamely mintastruktúrára, s ez okozhat téves hibajelzést
2. A teljesség
Teljesség: az „intuitíve” elvárt minden elem előállítható-e az axióma rendszer leírt műveletek által? E kérdés tehát nem a módszerre vonatkozik, hanem magára az axióma renszerre. Érdekes meggodolni azért, hogy mi módon lehetne „algoritmikusan” ellenőrizni ezt a fajta teljességet.
3. Praktikus kérdések
Néhány olyan kérdést vetek föl az alábbiakban, amelyek a módszer kidolgozása közben vetődtek föl. Alighanem hasznosak lehetnek a mindennapi használat során. Kérdések:
1. Hogyan készítsük el a típusosztály algebrai specifikációját?
2. Hogyan készítsük el a típusosztály P/P-specifikációját?
3. Többletállítások a típusosztályhoz, invariáns állítások
4. Egy bizonyítás nyomon követése a Prolog adatbázis-kezelő szolgáltatására építve
4. Ekvivalens formulák keresése
Az eddigi gondolatmenet egyik lényegi tulajdonsága az volt, hogy a kétféle rendszerben felállított állítások valamifajta kompatibilitását tudtuk kimutatni, feltéve, hogy megvolt. Most többre vágyunk, és az ekvivalencia reményével igyekszünk az algebraiból a P/P-rendszerbe áttérni. A [KV2001] irodalomban szereplő állítás erre jogalapot teremt.
|
|
Állítás: Az algebrai specifikáció elő- és utófeltételes formára
hozható. Bizonyítás: A bizonyítás konstruktív, amelyre
építhetünk a példánk esetében.. Konstrukció: …… a
bizonyítás lépései … |
Az eddigi kifogásunk a fenti átírással szemben az volt, hogy a P/P-specifikációban olyan hivatkozásokat tartalmaz (más operációkra), amelyek nem kívánatosak ilyen rendszerben. Ezen úgy segíthetünk, hogy a sorozat-nyelv [SzPG2002, PSzZs1998, SzP1999] elemeit fölhasználjuk, s mintegy a kapott formulák még nem kívánatos részleteinek megfeleltetjük a sorozat-nyelvbeli analogonját.
Figyeljük meg a verem esetén az áttérést! Időnként az axiómát kettébontjuk, s majd egyesítjük a specifikációdarabokat.
f0 = Üres. I(v)= 0£Hossz(v)[5]
|
Algebrai
axióma |
P/P-specifikáció1 |
P/P-specifikáció2 |
|
– |
Üres: |
Uf: 0£Hossz(v) Ù v=() |
|
Üres=v Û Üres?(v) |
|
|
|
Üres=v Þ Üres?(v) |
Üres?(v): |
|
|
Üres¹v Þ ØÜres?(v) |
Üres?(v): |
|
|
|
Üres?(v): |
|
Az axiómát két részre vágtuk, majd a egyesítettük az átírás eredményeit.
|
Ø Üres?(Verembe(v,e)) |
Verembe(v,e): |
Verembe(v,e): |
Látható nehézség: a Verembe konstrukciós művelet szempontjából nem veszi számításba az axióma tényleges mondanivalóját. Ha az Üres? szelekciós művelet szempontjából tekintenénk, akkor semmivel több információhoz nem jutnánk, mint amennyihez a korábbi axióma átírásával jutottunk.
Tető(Verembe(v,e))=e |
Tető(v): |
|
A sorozatnyelvre áttérés valójában két lépésben történt. Az első:
Ef: w=v&(e)
Uf: Tető(w)=e
Majd a w kiküszöbölésével kapjuk a végső átírtat.
Irodalom
Kozma L. – Varga L.: „Adattípusok osztálya.”, ELTE TTK Informatikai TanszékCsoport, 2001
Szlávi P. – Pap Gné: „Adatszerkezet – Típusok”, Informatika a felsőoktatásban’99 konferencia, Debrecen, 2002
Pap Gné – Szlávi P. – Zsakó L.: „Módszeres programozás – Adattípusok”, ELTE TTK Informatikai TanszékCsoport, 1998
Szlávi P.: „Programok, programspecifikációk.”, Informatika a felsőoktatásban’99 konferencia, Debrecen, 1999
Programhivatkozások
Szlávi P.: „A verem specifikációinak kompatibilitását ellenőrző Prolog program – strukturális indukció alapján; hibás Tető és Verembe operáció esetén.”,. http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/VERST3H2.PRO
Szlávi P.: „A verem specifikációinak kompatibilitását ellenőrző Prolog program – strukturális indukció alapján; hibás Tető és Verembe operáció esetén.”,. http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/VERST3H2.PRO