1. A kétféle specifikációról
Típusok (típuskonstrukciók), típusosztályok leírását gyakorta többféle absztrakciós szinten is elvégezzük [FH2002, SzPG2002, PSzZs1998]: haladva a legabsztraktabb (algebrai) felöl, a konkrétabb, külső felülettel (P/P-, export modullal) specifikálton át a megvalósítás apró részleteit is tartalmazó (modul-specifikáció vagy esetleg már konkrét programozási nyelven megírt) felé. Fontos tudnunk, hogy ezen inkrementális programfejlesztés közben megtett lépéseink korrektek abban az értelemben, hogy ugyanazt a típust írják le mindannyian eltérő nyelvi szabályok között (értsd: formalizmus mellett), eltérő „részletességgel”.
Az elkövetkezőkben villanásszerűen utalunk a két, számunkra most fontos specifikációs „nyelvezetre”: az algebrai [GN1986] és a P/P-specifikációra [SzZs2000], hogy azután vizsgálhassuk a Prolog programban történő egyesítésük lehetőségét. [SzP1999]
1.1. Algebrai specifikációs nyelv
1.1.1. A típus algebrai leírásának kerete
A típusosztály legfelsőbb szintű megragadását jelenti az algebrai leírás, amely „csak” annyit igyekszik lerögzíteni, hogy a típushoz asszociált műveletek jellegzetes kombinációi milyen, a tesztelő operációkkal érzékelhető változásokat eredményeznek a középpontba helyezett adatszerkezeten. Az algebrai specifikáció csupán axiómákat állít föl. Tehát az adatábrázolástól éppúgy távol marad, mint az algoritmikus megvalósítástól.
Algebrai specifikációhoz számos „nyelvezet” létezik. (Pl. [KV2001]) Az alábbi táblázatba annak az algebrai leírásnak a szintaktikai minimumát foglaltuk, amelyet az ELTE Informatika tanárszakán használunk.
|
Szintaktikai „minta” |
Magyarázat |
|
TípusKonstrukció(paraméterek): Asszociált műveletek: Operáció(Értelmezési tartomány):
Értékkészlet … |
A
definiálandó típuskonstrukció „alkalmazási sablona” (feje). Operációinak
szignatúrája (értelmezési tartománya, értékkészlete) |
|
Axiómák: Jelölések: · objektum: Típus(paraméterek) = értelmező megjegyzés · … 1o … az axióma informális szövege vagy megnevezése... a formalizált axióma 2o … … |
Az operációk kapcsolatát leíró
axiómák, és a bennük fölhasznált objektumok „deklarációi”. Esetleg kibővítve fontos
következményállításokkal. |
1.1.2. Implicit error-axiómák
Mivel a specifikálás során foglalkozni kell az operációk (nem kizárható) illegális használatával, annak körülményeivel, be kell vezetni egy „univerzális” NemDef értéket.[2] Egy operációt „eredménnyel” (más szóval: legálisan) nem használhatunk egy NemDef értékű (azaz egy hiba-állapotba jutott) adatra. Ezt mondja ki az error-axióma. Ezt az axiómát a továbbiakban nem szerepeltetjük explicite az egyes operációkkal kapcsolatban, ezért minősítjük implicitnek.
Az adatok létrehozás előtti állapota is a NemDef. (Iniciális error-axióma)
Dolgozatunkban egy közismert példát követünk végig: a verem típuskonstrukció (közismertebb néven: verem-osztály) példáját. Lássuk a verem algebrai leírását!
Példa:
|
|
Verem(Típus Elem): Asszociált műveletek: Üres:
Verem Üres?(Verem):
Logikai
Tető(Verem):
Elem È {NemDef} Verembe(Verem,Elem):
Verem È {NemDef} Veremből(Verem):
( Verem x Elem ) È {NemDef} Axiómák: Jelölések: · v,v': Verem(Elem) = veremtípusú
objektum · e,e': Elem = elemtípusú objektum 1o Üres –
axióma Üres?(Üres) 2o Üres? – axióma Ø Üres?(Verembe(v,e)) 3o
Tető–Verembe – axióma Tető(Verembe(v,e))=e 3’o Tető –
hiba-axióma Üres?(v) Þ
Tető(v)=NemDef 4o Veremből –
axióma Veremből(Verembe(v,e))=(v,e) Ù 4’o Veremből –
hiba-axióma Üres?(v) Þ Veremből(v)=NemDef |
1.2. A külső felület szerinti specifikáció
1.2.1. A típus P/P-specifikáció kerete: a modul
Az algebrai specifikációhoz képest fontos eltérés, hogy amíg az algebrai elvárásaink egyetlen összefüggő rendszert (axiómarendszert) alkotnak, addig a külső felület szerinti specifikáció esetében minden egyes operáció egymástól független, önálló „egységet”, mikrórendszert alkot.
ExportModul TípusNév(InputParaméterek)[3]
Konstans [Ritkán van
ilyenre szükség.]
Kons1,Kons2,... [a TípusNév típus néhány kiemelendő
konstansa]
Függvény Fv1(FormParam):
FvTip1
Ef: az Fv1 alkalmazhatóságának
feltétele
Uf: az Fv1 által elvégzett
transzformáció
...
Eljárás Elj1(FormParam)
Ef: az Elj1 alkalmazhatóságának
feltétele
Uf: az Elj1 által elvégzett
transzformáció
...
Operátor Op1(FormParam):
OpTip1
Ef: az Op1 alkalmazhatóságának
feltétele
Uf: az Op1 által elvégzett
transzformáció
...
Modul vége.
Az operációk közötti kapcsolatot a típust meghatározó adatok jelentik. Ezen adatokat transzformálják, elemzik az egyes operációk. Itt tehát már nem kerülhető el, amit eddig ügyesen figyelmen kívül hagytunk: az ábrázolás. Törekszünk természetesen még mindig kellően általánosan fogalmazni.
1.2.2. P/P-specifikációbeli formalizmus: a sorozatnyelv
Az általunk vizsgált típusok (osztályok) mindegyikénél egy sorozat játszik majd középponti szerepet. Ezért alkalmazunk az elő- és utófeltételben egy „sorozatnyelv”-nek nevezett formalizmust. E formalizmusban a sorozatok kezeléséhez az alábbi műveleteket eleve definiáltnak vesszük:
· ( ) – üres sorozat,
· si – i. eleme az s sorozatnak,
· |s| – az s sorozat hossza, elemszáma,
· (s1,..,si) – a sorozat első i db eleméből alkotott (rész)sorozat,
· (si,..,s|s|) – a sorozat i. elemével kezdődő (rész)sorozat,
· s&t – az s és a t sorozat elemeinek egymásután illesztése.
Minden összetett szerkezetet ennek a nyelvezetnek a „logikája” szerint jelölünk. Így járunk el a direktszorzat esetében is: Például: AxBxC halmaz egy elemét (a,b,c) jelöli, ahol természetesen elvárható, hogy aÎA, bÎB, cÎC teljesül.
Az algebrai leírásban –mint láttuk– előbukkan olyan szituáció, amelyben a típusba tartozó adat nemdefiniált értékűvé vált, azaz hiba állapotba jutott. Ezt az állapotot hivatott rögzíteni az adatszerkezet egy logikai komponense. Tehát minden általunk leírt típusú adatnak minimum két komponense lesz: egy, az elemek sorozatát tartalmazó, és egy hibásságot rögzítő logikai komponens – TElem*xLogikai.
A verem export modulja [SzP1999, PSzZs1998] következik az alábbi példában.
Példa:
ExportModul Verem(Típus TElem):
[Jelölések a specifikációhoz:
1) Verem=SorozatxHiba, Sorozat=TElem*,
Hiba=Logikai
2) v' a Verem művelet utáni állapota,
ha a bemenetitől meg kell
különböztetni]
Eljárás
Üres(Változó v:Verem)
[veremlétrehozás
a memóriában]
Ef: Ø$vÎVerem
[4]
Uf: $vÎVerem
Ù
v=((),Hamis)
Függvény
Üres?(Konstans
v:Verem): Logikai
[üres-e
a verem]
Ef: $vÎVerem
Ù
Øv.hiba
Uf: Üres?(v)=(v.sorozat=())
Függvény
Tető(Változó
v:Verem): TElem
[a
verem tetőelemének értéke]
Ef: $vÎVerem
Ù
Øv.hiba
Uf: v.sorozat=(v1,...,vn)
Þ
Tető(v)=vn
v.sorozat=() Þ
v'.hiba=Igaz
Eljárás
Verembe(Változó
v:Verem, Konstans
e:TElem)
[verembetétel]
Ef: $vÎVerem
Ù
Øv.hiba
Uf: v.sorozat=(v1,...,vn)
Þ
v'.sorozat=(v1,...,vn,e)
Eljárás
Veremből(Változó
v:Verem, e:TElem)
[a
tetőelem kivétele]
Ef: $vÎVerem
Ù
Øv.hiba
Uf: v.sorozat=(v1,...,vn)
Þ
v'.sorozat=(v1,...,vn-1) Ù e=vn
v=() Þ v'.hiba=Igaz
Függvény
Hibás?(Változó
v:Verem): Logikai
[történt-e
hiba a veremre hivatkozás
során, „törli” a hibaváltozót]
Ef: $vÎVerem
Uf: Hibás?(v)=v.hiba
Ù
v'.hiba=Hamis
Modul vége.
1.2.3. A P/P-specifikáció algebraiba beilleszthetőségének megsejtése
Van tehát kétféle leírása a típusnak: egy összefüggő algebrai rendszer, axiómákból; valamint egy formálisan egyáltalán nem összefüggő P/P-specifikációkból álló mikrórendszerek halmaza.[5] Az egymáshoz illeszkedés alatt értsük azt, hogy ha feltesszük a mikrórendszerek helyességét (azaz hogy, ha az előfeltétel teljesül, akkor az utófeltétel is teljesül), akkor azon axiómák is teljesülnek, amelyekben az adott mikrórendszerek szerepelnek.
Például, tegyük föl a Veremből és a Verembe operációk P/P-specifikációinak helyességét, akkor az 4o axióma is teljesül. A vizsgálandó állítás ekkor így hangzik:
Ha a
Verembe(v,e)
Ef: $vÎVerem Ù Øv.hiba
Uf: v.sorozat=(v1,...,vn) Þ v'.sorozat=(v1,...,vn,e) [6]
Veremből(v,e)
Ef: $vÎVerem Ù Øv.hiba
Uf: v.sorozat=(v1,...,vn) Þ v'.sorozat=(v1,...,vn-1) Ù e=vn
v=() Þ v'.hiba=Igaz
P/P-specifikációk
helyesek, akkor teljesül a
„4o Veremből – axióma” is, azaz a
Veremből(Verembe(v,e))=(v,e) Ù
Ø
Üres?(v) Þ Verembe(Veremből(v))=v
Az egyszerűség kedvéért elégedjünk meg az axióma első felének ellenőrzésével, azaz a Veremből(Verembe(v,e))=(v,e) formula teljesülésének belátásával!
Első lépésként a Verembe operációt kell figyelembe vennünk. Ennek előfeltételét ($vÎVerem Ù Øv.hiba), s az utófeltétel (v.sorozat=(v1,...,vn) Þ v'=(v1,...,vn,e)) elfogadjuk. A verem-állapot utófeltételben szereplő bemeneti és kimeneti állapotát egybe vetve (s az előfeltétel Øv.hiba részét tudomásul véve) az utófeltétel a következő alakban is írható:
(1) v'.sorozat=v.sorozat & (e).
Másodikként
a Veremből operációt elemezzük
észrevéve, hogy ez esetben legalább 1-elemű sorozatra kell alkalmazni. Hasonló
gondolatmenettel az utófeltétel itt is tömöríthető: v.sorozat =v'.sorozat&(vn) Ù e=vn, sőt még tovább:
(2) v.sorozat=v'.sorozat&(e).
Harmadik lépésben kövessük az axióma kiértékelését! Hogy
elkerüljük az adatok keveredését, az egyes műveletek paramétereit indexeljük: 1
indexszel a Verembe művelet paramétereit és 2-vel a Veremből műveletét.
|
Bemenet |
Verembe |
Kimenet |
(1)-ből |
|
(3) |
|
(v1.sorozat, |
® |
v1’.sorozat |
= |
v1.sorozat&(e1) |
= |
|
|
= |
v2.sorozat |
® |
(v2'.sorozat, |
|
|
|
|
Bemenet |
Veremből |
Kimenet |
|
Szedjük össze az adatok
közötti kapcsolatokat!
A Verembe-Veremből műveletek közötti paraméterátadás:
|
(3) |
v1.sorozat&(e1) |
= |
v2.sorozat |
A teljes transzformáció (Bemenet®Kimenet):
|
(BeKi) |
(v1.sorozat,e1) |
Veremből·Verembe |
(v2’.sorozat,e2) |
Az axióma:
|
(Ax) |
(v,e) |
Veremből·Verembe |
(v,e) |
A (2) v2-re
aktualizált alakja:
|
(22) |
v2.sorozat |
= |
v2'.sorozat&(e) |
A (BeKi)–ből rögvest
látszik, hogy a 2. komponensbeli e identikusan transzformálódik –ahogy (Ax) el is várná–, ha e1=e2
teljesül, amit semmi sem tilt. Tehát feltesszük. A fenti kapcsolatokban ezért ei
helyettesíthető e-vel. Belátandó, hogy az 1. komponensbeli v is
változatlan marad.
A (3) miatt v2.sorozat helyett írhatjuk: v1.sorozat&(e1), de a (22)-vel összevetve v2'.sorozat-ra az adódik, hogy
meg kell egyezzék v1.sorozat-tal, ami a (BeKi) bemenetén szerepelt
a sorozat-komponensként, s éppen ezt vártuk.
2. Prolog nyelvi minimum
Az alábbiakban a Borland által kifejlesztett Turbo Prolog nyelvjárásról esik néhány, összefoglaló szó. [RKRB1988] Legfontosabb szintaktikus tudnivalókat az alábbi Prolog nyelvű programvázlat tartalmazza:
Domains
/*
A predikátumok (tények, szabályok) paramétertípusainak definiálása.
Általános alakja: ’típus = típuskonstrukció’. */
unio = funktor1(típus1); funktor2(típus2); …
iter = típus*
dirSzor = funktor(típus1,típus2,…)
…
Predicates
/*
A tények és szabályok szignatúrájának (fejsor-szintaxis) deklarálása; minden,
később előkerülő tény és szabály itt deklaráltatik:
*/
ténySzabály(típusok felsorolása)
…
Database [7]
/*
A "dinamikusan" kezelendő tudás: szabályok.
Elhagyható szekció; de ha van, akkor nem lehet közös része a
'Predicates'-szel.
*/
ténySzabály(típusok felsorolása)
Clauses
/*
Tények és szabályok:
*/
tény(szignatúrának megfelelő
paraméter-lista).
…
szabály(szignatúrának megfelelő
paraméter-lista)
if logikai formula.
…
Goal
/*
A feladat megoldását „elindító” állítás:
*/
logikai formula.
A tények: végülis névvel ellátott relációk. A megnevezett relációba hozzuk a paraméterként felsorolt (konstans) adatokat. A szabályok szintén névvel ellátott relációk, csakhogy a relációba bizonyos feltételekkel kerülnek a paraméterlistában felsorolt adatok. Ezek az úgynevezett: Horn-klózok.
Alakjuk: „Következmény(paraméterek) Ü feltétel(paraméterek)”, ahol a „Ü” műveleti jel a szokástól eltérő irányú implikáció, a következmény: egy „nevesített” paraméteres szabály, a feltétel bizonyos korlátozásokkal negációt is tartalmazhat, de jellemzőbben konjunkciót, ill. diszjunkciót. Értelemszerűen a paraméterek most nem egyetlen „pontját” jelölik ki a sokdimenziós paramétertérnek, hanem egy alterét. Más szóval: legalább egy paramétere nem konstansként lett rögzítve.
Jelentésük: a következmény teljesül (azaz a paraméterként felsorolt konstansok az adott nevű relációban állnak egymással), ha a feltétel igaz.
A későbbiek során Turbo Prolog program futásáról készült „pillanatfelvételekkel” is találkozunk, amelyek az alábbi ábrához nagyon hasonlatosak lesznek.
Az Editor „ablak” mutatja a forrásprogram egy darabkáját, míg a Dialog a program eredményét keretezi. (Ha látszanak is majd egyéb ablakok, számunkra lényegtelenek lesznek.)
|
|
|
3.1.
ábra – Turbo Prolog program fejlesztői környezetének felépítése |
3. Átírási szabályok
3.1. Algebrai és P/P-specifikáció mint egyetlen szabály-gyűjtemény
A Prolog-ban tehát minden tényként esetleg szabályként jelenik meg. Tehát át kell tudnunk írni az algebrai axiómáinkat éppúgy, mint a modulokban szereplő operátorok egyedi elő- és utófeltételre szétválasztott specifikációit. Ráadásul ezeket egyetlen rendszerré kell összekovácsolnunk, hogy vizsgálhassuk: mennyire működnek együtt.
3.2. Az operátor-szabály szignatúrája
Az operátor az algebrai leírásban egységesen függvényként jelenik meg. Értékkészlete gyakorta halmazok uniójaként, sőt néha halmazok direktszorzataként bukkan elő. Pl.: VeremÈ {NemDef}, vagy VeremxElem.
Mivel a vizsgálatunk szempontjából teljesen lényegtelen, hogy a típuskonstrukciók milyen elemtípuson nyugszanak, feltehetjük, hogy a bázistípus mindig (pl.) egész szám típus legyen.
A Prolog direktszorzat képzése ekként oldható meg: „hF(h1,h2,…)”., ahol hF – funktor, hX – komponens-típus.
Az unió megfelelője: „h1F(h1); h2F(h2);..”., ahol hXF – funktor, hX – alternatíva-típus.
Egy felsorolás típus az unió speciális, leegyszerűsített váltózatának is tekinthető, így átirata: „k1; k2;..”., ahol kX – alternatív konstansok.
Az iterált Prolog-beli párja: „h*”, ahol h – a bázistípus.
A fenti Prolog megfeleltetések ismeretében vermes példánk legbonyolultabb, „veremből” operáció szignatúrájában szereplő halmazok leírhatók. Mielőtt ezt megtennénk, meg kell gondolni, hogyan ültessük át a Prolog programba az operációkat. A probléma nyilvánvaló: a Prolog-ban minden tevékenység szabályként, tehát logikai értékkel rendelkező számítással fogalmazandó meg. Tehát a döntés egyértelmű:
Operátor(Értelmezési tartomány): Értékkészlet
Prolog párja:
Operátor(Értelmezési tartomány , Értékkészlet)
szignatúrájú szabály lesz.
Lehetnek a fenti általános operátor-sémától eltérő szignatúrájúak is: konstruktorok, illetve destruktorok. Ezek Prolog-megfelelői:
Konstruktor: Értékkészlet
Prolog párja:
Konstruktor(Értékkészlet)
szignatúrájú szabály lesz.
Destruktor(Értelmezési tartomány)
Prolog párja:
Destruktor(Értelmezési
tartomány)
szignatúrájú szabály lesz.
Így már az operátorokat könnyedén átültethetjük a Prolog-ba, ha észrevesszük, hogy a NemDef érték mindig a verem „kóros” állapotára utal. Elegendő tehát a verem –ezidáig homályos– alap típusát bővíteni a {NemDef,Def} halmazzal. A verem tehát a veremelemek sorozatából[8] és a hibásságot jelző logikai érték kettőséből fog állni.
Mivel a verem állapotának szerves jellemzőjévé tettük a „kórosságot” jelző komponenst, ezért olyan operációk szabályában is fel fog bukkanni outputként a verem, amelyben eredetileg csak az inputon szerepelt (pl. Tető).[9]
Domains
TNemDef = nemDef; def
TElem = Integer
TVerem = TElem*
TVeremK = verem(TVerem,TNemDef)
TLogikai = igaz; hamis
Predicates
ures(TVeremK)
uresE(TVeremK /*input*/,
TLogikai /*output*/)
teto(TVeremK, /*input*/
TElem,TVeremK /*output*/)
verembe(TVeremK,TElem, /*input*/
TVeremK /*output*/)
verembol(TVeremK, /*input*/
TElem,TVeremK /*output*/)
3.3. Az algebrai leírás szabályokká alakítása
A „logika” kódolásához meg kell gondolnunk az alábbiakat:
1. az algebrai specifikációban ki nem mondott (implicit) error-axióma megfogalmazása operációról operációra (és az iniciális error-axióma)
2. az algebrai axiómák mechanikus átírása
3. az egyes operációk PP-specifikációjának Prolog-osítása
3.3.1. Implicit error-axiómák Prolog szabályai
Azt kell kifejeznünk, hogy ha a verem állapota (2. komponense) NemDef, akkor a transzformáció tényleges számolás nélkül, „üresen” hajtódik végre:
Operátor(verem(_,nemDef),
/* input veremparaméter */
_, … , /* további input paraméterek */
verem(_,nemDef), /* output veremparaméter: változatlan */
_, … ) /* további
output paraméterek */
Ezt tehát minden egyes operációra ki kell mondani!
Példák:
uresE(verem(_,nemDef),_). /* ÜresE-implicit
error-axióma */
teto(verem(V,nemDef),_,verem(V,nemDef)). /* Tető-implicit error-
axióma */
Magyarázat
a két példához: az ÜresE
operációt a NemDef
állapotú veremre alkalmazva, nincs
szerepe az axióma igaz-értéke szempontjából sem a veremelemek sorozatának, sem
az operáció által visszaadott éréknek. Ehhez hasonlóan a Tető operációt a NemDef állapotú veremre alkalmazva, az
axióma „sikere” független kell legyen a második paraméter (a Tető által visszaadott érték)
milyenségétől. Érdekes különbséget vehetünk észre a két példa paraméterezésében.
Mindkettőben a veremelemek sorozata számunkra érdektelen, de amíg az elsőben
a szabad paraméter „_” jelével élhettünk, addig a Tető példájában nem tehettük. Oka: ebben a szabályban hangsúlyoznunk
kell, hogy a bemeneti és a kimeneti struktúrában a két paraméterértéknek meg
kell egyezniük. Azaz bármi lehet a sorozat, de a kimenetkori azonos a
bemenetkori értékkel.
3.3.2. Iniciális error-axióma szerepe
Mivel annak vizsgálata, hogy valamely operációt ideje korán (az
adat létrehozását megelőzőleg) hajtottunk-e végre, nem különösebben nehéz
feladat, ezért eltekintünk ennek számbavételétől.[10] Ha tehát valamely operáció
előfeltételei között szerepel az „operálandó adat létezésére vonatkozó
feltétel”, akkor azzal nem foglalkozunk.
3.3.3. Algebrai axióma Prolog szabálya
Filozófiánk lényegi kérdéséhez érkeztünk el. Hogyan is ellenőrizzük a kétféle specifikációból származó szabályok ellentmondás-mentességét? Egy lehetséges út vázlata a következő:
Mivel vizsgálatunk olyan típusra vonatkozik, amelyben valamilyen sorozat kezelését végzik a típusműveletek, és az axiómákban éppúgy, mint a P/P-szabályokban az üresség feltétele, valamint a definiáltság tűnik föl unos-untalan, ezért két szignifikáns esetet különböztetünk meg: az üres sorozat esetét, meg a nem üreset. S mindkettőn belül önálló aleset: legális vagy illegális állapotú-e a kiinduló sorozat. Az utóbbiban az az eset testesül meg, amikor valamilyen hiba folytán az adatszerkezet NemDef állapotba jut. A kérdés ekkor: ebben a helyzetben az operációk mit tesznek az adatta. Mivel ekkor megállapodás szerint bármely operáció transzformáció nélkül „működik”, amit az implicit error-axióma szerint kell kódolnunk, így azon axiómák, amelyekben szerepelnek, nagy eséllyel nem fognak teljesülni. Ez a negatív eredmény azonban semmi információt nem hordoz. (Sőt a ritka teljesülése sem.) Ezért nem fogjuk a NemDef állapotot külön tesztesetben vizsgálni.
Az algebrai specifikáció axiómáit tekintsük olyan szabályoknak, amelyeknek két paramétere van: az egyik a kiinduló struktúra (amely lehet üres, vagy nem üres; lehet NemDef vagy Def állapotban); a másik explicite fejezi ki az algebrai axióma teljesülését (Igaz) vagy nem teljesülését (Hamis). Szignatúrája:
Axióma(TVeremK
/*mintastruktúra*/,TLogikai /*teljesül-e*/)
A szabály
meggondolást igénylő része, a klóz feltételrésze. Ez lesz az algebrai axiómában
szereplő logikai kifejezés Prolog-os párja. Vizsgálni kell a „megengedett
állapotban” levő, legális adatokra (Def) és az illegálisokra (NemDef) vonatkozó alkalmazás esetét. Az illegális értékelése egyszerű,
hiszen ilyen adatokra alkalmazáskor nem fog az axióma sérülni; ugyanis a
definiáltság vagy nemdefináltság kérdését az axiómákon belül rögzítjük.
Példa:
|
Algebrai
specifikáció egy axiómája |
Az axióma szabályalakja |
|
1o Üres –
axióma
Üres?(Üres) |
Predicates … … Clauses … axioma1(V,igaz) if ures(V) and
uresE(V,igaz). /* nemDef-re:Igaz */ axioma1(_,hamis). |
Olyan algebrai axiómák esetén, amelyben jól elválasztható részekre bontható az állítás, mindegyikhez önálló szabályt kell fogalmazni. (Ez később általánosan követendő elvvé fog válni!)
Példa:
|
Algebrai
specifikáció egy axiómája |
Az axióma szabályalakja |
|
Veremből(Verembe(v,e))=(v,e) Ù |
Predicates … Clauses … axioma4(V,igaz) if axioma4(_,hamis). axioma4_1(V,igaz) if verembe(V,E,W) and
axioma4_2(V,igaz) if uresE(V,hamis) and
|
|
|
Megjegyzés:
az axióma4_2 kódolásánál
egy implikáció Prolog megfelelőjét kellett megtalálnunk. Erről később lesz még szó. Illetve a „ØÜres?(v)” tagadás helyett az ellenkezőjét állítottuk. |
3.3.4. P/P-specifikáció Prolog szabálya
Itt válik elkerülhetetlenné a döntés a TVerem típus mibenlétéről: legyen TElem bázistípusú sorozat. A sorozatok kezelése a konkrét feladatunktól független, előre kidolgozható. Az alábbi eszközkészlet tartozik, előre definiáltként, a programhoz include-ként hozzáilleszthetőként[11]:
· Elem(sorozat,i) – i. eleme a sorozatnak,
· Hossz(sorozat) – sorozat-hossz,
· Eleje(sorozat,i) – a sorozat első i db eleméből alkotott (rész)sorozat,
· Vége(sorozat,i) – a sorozat i. elemével kezdődő (rész)sorozat,
· EgymásUtán(sorozat1,sorozat2) – a két sorozat elemeinek egymásután illesztése.
A példánk esetében nincs is szükség a fenti speciális kezelő műveletekre, elegendőek a Prolog eleve meglévő sorozat-kezelő eszközei.
Visszatérve a P/P-átírásra, logikusnak látszik olyan szabály hozzárendelése, amelyben az utófeltételben leírt állapotot a szabály következmény paramétereivel rögzítjük –ha lehet–, s az előfeltételt pedig a szabály „if” utáni feltétel részében fogalmazzuk meg.
Példa:
|
Operáció
P/P-specifikációja |
Operáció szabálya |
|
Függvény Üres?(Konstans v:Verem): Logikai |
uresE(verem([],D),igaz) if |
|
Megjegyzés:
az előfeltétel egy részletének áthúzásával jeleztük, hogy az átírásban nem
játszik szerepet. |
A
2. paraméter típusa: Logikai.
Ezért kézenfekvő 2 szabály-alternatívában gondolkodni. Egyik az „igaz”, másik a „hamis” értékhez tartozik. A
szabály első alternatíváját egyszerűbben is írhatjuk.Ha kihasználjuk, hogy D¹nemDef ugyanaz,
mint D=def. Íme: |
|
|
uresE(verem([],def),igaz). |
Olyankor, amikor az utófeltétel több kijelentést egyesít, az egyes kijelentéseket önálló szabály-alternatívaként kell megfogalmazni. Ez akkor könnyen felismerhető, ha az utófeltétel implikációk konjunkciója. Sokszor az implikáció feltételrésze a szabály paraméterlistájában (illesztési feltétel gyanánt) helyezhető el. Máskor a szabály feltételrészében kell a komplett implikációt kódolni.
Példa:
|
Operáció P/P-specifikációja |
Operáció szabálya |
|
Függvény Tető(Változó
v:Verem): TElem |
teto(verem([Vn|V],def),Vn, teto(verem([],def),_, |
Megjegyzés: valóban alternatívával kódolható, hiszen a feltételek egymást kizárják, azaz közülük csak egyetlen egy lehet igaz.
3.4. Az implikáció kódolása
A végső egyesítésnek már talán csak egyetlen akadálya maradt[12], amely több helyen is fölvetődhet: hogyan ültethető át egy implikációt tartalmazó formula? A Prolog leírási és végrehajtási szabályait figyelembe véve a redundánsnak tűnő „A Þ B” ® „A Ù B Ú ØA” (ekvivalens) helyettesítéssel élünk.
Például (4o algebrai axióma részlete –ahogy már láttuk–):
|
implikáció |
szabály |
|
Ø Üres?(v) Þ
Verembe(Veremből(v))=v |
uresE(V,hamis) and
|
Hasonló problémát kell megoldani a két hiba-axiómánál. Nagyon fontos, hogy a későbbi –esetleges– transzformációk során is megmaradjon az implikáció integritása! (L. még itt!)
3.5. A szabályok programmá egyesítése
Egyetlen kérdés maradt hátra: hogyan késztethető a Prolog rendszer arra, hogy az eddig egybe fésült szabályrendszer illeszkedését kimutassa. A válasz roppant egyszerű: célállításként fogalmazzuk meg (2-2, korábban megfogalmazott paraméterrel) az axiómák konjukcióját, s írjuk ki a kiszámítás után kapott paraméter értéket. Ideális esetben minden axiómára mind üres, illetve nem üres (s ahogy már megindokoltuk: csak „legális” állapotú) adatra „igaz” lesz a válasz. Valahogy így:
Példa:
Goal
/*(üres,def)-re igaz-e:*/
V0X=struktura([],def) and
axiomaX(V0,JoE0X) and
write("X:",JoE0X) and
write(" ",V0X,"-re") and nl
and
/*(nem üres,def)-re
igaz-e:*/
VX =struktura([_],def) and
axiomaX(VX,JoEX) and
write("X:",JoEX) and
write(" ",VX,"-re.") and nl
…
Egy apró megjegyzés a kódolás könnyebb megértéséhez: furcsa azonosítójú változókkal találkozhatnunk a célállításban. A kulcs ennyi: „V” veremről van szó, „0” üres, vagy ha a nulla elmarad, akkor nem üres, „X” az X-edik axióma tesztelésében vesz részt. Például: „V01” = „olyan verem, amely 0 darab eleme van, és az 1. axióma tesztelésében vesz részt”, „V2” = „azt a veremet jelöli, amely nem üres (nincs 0 az azonosítóban), és a 2. axióma teszteléséhez használjuk”… A Prolog logikájából fakadóan nincs mód ugyanazon változó kétféle értékkel tőrténő „újrafelhasználásra”. Emiatt nem hagyható el az „X” az azonosító nevéből.
A fentiek alapján a kódolás hiánytalanul elvégezhető. Vegyük észre, hogy a Hibás? operátor elő sem bukkan az axiómákban, ugyanis a specifikáció algoritmikus lépésében született. Hiába van rá vonatkozó (operátor-) szabály, az a Prolog program számára láthatatlan, tesztelhetetlen marad, hiszen a célállítás axióma-centrikus: nincs axióma, amely „mozgásba igyekezné hozni”. Két dolgot tehetünk: vagy utólag hozzávesszük ezt az operátort az algebrai leíráshoz, és újabb axiómával fejezzük ki a vele szembeni elvárásainkat[13], vagy nem vesszük figyelembe a kompatibilitás ellenőrzésekor. Most az utóbbit választjuk, mondván: nem valamifajta ekvivalenciát tartozunk bizonyítani, hanem a P/P-specifikáció algebraihoz illeszkedését; másrészt egyszerű működése könnyen, szemmel is ellenőrizhető.
Egyetlen fontos megjegyzést kell még tennünk. Mivel az a cél, hogy a specifikáció esetleges hibáira a Prolog program ellenőrzött vágányokon maradjon, s úgy mutassa ki ezeket, számolnunk kell a Prolog alapvető hozzáállására: backtrack-kel keresi az illeszkedő mintát. Tehát ahol garantáltan értelmetlen a backtrack, ott meg kell akadályozni a visszalépést. Így kell tenni –nyilvánvalóan– a célállítás egyes logikailag független részei között, de az axiómák esetében is számos helyen.
A megakadályozás Prolog eszköze a vágás. A vágás operátor működése két ponton is befolyásolja a végrehajtást:
1. a szabályban a vágás előtti formulákra már nem tér vissza, és a szabály Fail-lel zárul;
2. továbbá a szabály eddig még nem vizsgált alternatíváit sem fogja vizsgálni.
Emiatt a vágást tartalmazó algebrai axiómákhoz tartozó szabályok utolsó, egyébként éppen az algebrai axióma sérülését kijelentő alternatívára nem kerülhet a sor. Ez komoly gond. Kikerülésére persze van mód: egyesítsük egy önálló „al-szabályban” a vágást tartalmazó formulát, s így annak (egyébként nem levő) alternatívái maradnak ki a visszalépéskori végrehajtásból, de az egy szinttel feljebbi „axiomatikus” szabály további alternatívái zavartalanul érvényesülhetnek. Ügyelni kell persze arra, hogy az implikációk kódolásánál két ágra szakadt kód-darabok egyetlen al-szabályban maradjanak.
Példa:
|
szabály vágással |
szabály korrekt vágással |
|
axioma3(V,igaz) if |
axioma3(V,igaz) if axioma3_1(V,igaz) if |
S egy implikációt tartalmazó példa:
|
szabály vágással |
szabály korrekt vágással |
|
axioma3H(verem(_,def),igaz)
if |
axioma3H(verem(_,def),igaz)
if Axioma3H_1(verem(_,def),igaz)
if |
Végezetül következzék a veremnek a Prolog rendszerben egyesített specifikációja!
Példa:
Domains
TNemDef = nemDef; def
TElem = Integer
TVerem = TElem*
TVeremK = verem(TVerem,TNemDef)
TLogikai = igaz; hamis
Predicates
ures(TVeremK)
uresE(TVeremK /*input*/,
TLogikai /*output*/)
teto(TVeremK, /*input*/
TElem,TVeremK /*output*/)
verembe(TVeremK,TElem, /*input*/
TVeremK /*output*/)
verembol(TVeremK, /*input*/
TElem,TVeremK /*output*/)
axioma1(TVeremK,TLogikai
/* teljesül-e */)
axioma1_1(TVeremK,TLogikai /*
teljesül-e */)
axioma2(TVeremK,TLogikai /* teljesül-e
*/)
axioma2_1(TVeremK,TLogikai /*
teljesül-e */)
axioma3(TVeremK,TLogikai /* teljesül-e
*/)
axioma3_1(TVeremK,TLogikai /*
teljesül-e */)
axioma3H(TVeremK,TLogikai /*
teljesül-e */) /* hiba-axióma */
axioma3H_1(TVeremK,TLogikai /*
teljesül-e */) /* hiba-axióma */
axioma4(TVeremK,TLogikai /* teljesül-e
*/)
axioma4_1(TVeremK,TLogikai /*
teljesül-e */)
axioma4_2(TVeremK,TLogikai /*
teljesül-e */)
axioma4(TVeremK,TLogikai /* teljesül-e
*/)
axioma4H(TVeremK,TLogikai /*
teljesül-e */) /* hiba-axióma */
axioma4H_1(TVeremK,TLogikai /*
teljesül-e */) /* hiba-axióma */
Clauses
ures(verem([],def)).
uresE(verem(_,nemDef),_).
/* ImpErrAx */
uresE(verem([],def),igaz).
uresE(verem([_],def),hamis).
uresE(verem([_|_],def),hamis).
teto(verem(V,nemDef),_,verem(V,nemDef)). /* ImpErrAx */
teto(verem([E|V],def),E,verem([E|V],def)). /* PP */
teto(verem([],def),_,verem([],nemDef)). /* PP: Err */
verembe(verem(V,nemDef),_,verem(V,nemDef)). /* ImpErrAx */
verembe(verem(V,def),E,verem([E|V],def)).
/* PP */
verembol(verem(V,nemDef),_,verem(V,nemDef)). /* ImpErrAx */
verembol(verem([E|V],def),E,verem(V,def)). /* PP */
verembol(verem([],def),_,verem(_,nemDef)). /* PP: Err */
axioma1(V,igaz) if
axioma1_1(V,igaz).
axioma1(_,hamis).
axioma1_1(V,igaz) if
ures(V) and uresE(V,igaz).
axioma2(V,igaz) if
axioma2_1(V,igaz).
axioma2(_,hamis).
axioma2_1(V,igaz) if
verembe(V,_,verem(W,def)) and
! and
uresE(verem(W,def),hamis).
axioma3(V,igaz)if
axioma3_1(V,igaz)
axioma3(_,hamis).
axioma3_1(V,igaz) if
verembe(V,E,W) and ! and
teto(W,E,W).
axioma3H(verem(_,def),igaz) if
axioma3H_1(verem(_,def),igaz).
axioma3H(_,hamis).
axioma3H_1(verem(_,def),igaz) if
uresE(verem(_,def),igaz) and
! and
teto(verem(_,def),_,verem(_,nemDef)
or
uresE(_,hamis).
axioma4(V,igaz) if
axioma4_1(V,igaz) and
axioma4_2(V,igaz).
axioma4(_,hamis).
axioma4_1(V,igaz) if
verembe(V,E,W) and ! and
verembol(W,E,V).
axioma4_2(V,igaz) if
uresE(V,hamis) and ! and
verembol(V,E,W) and ! and verembe(W,E,V)
or
uresE(V,igaz).
axioma4H(verem(_,def),igaz) if
axioma4H_1(verem(_,def),igaz).
axioma4H(_,hamis).
axioma4H_1(verem(_,def),igaz) if
uresE(verem(_,def),igaz) and ! and
verembol(verem(_,def),_,verem(_,nemDef)
or
uresE(_,hamis).
Goal
clearwindow and
/* 1. axióma tesztje: */
/*(üres,def)-re igaz-e:*/
V01=verem([],def) and
axioma1(V01,JoE01) and
write("1:",JoE01) and
write(" ",V01,"-re") and nl
and ! and
/*(nem üres,def)-re igaz-e:*/
V1=verem([_],def) and
axioma1(V1,JoE1) and
write("1:",JoE1) and
write(" ",V1,"-re.") and nl
and ! and
… /* … és a többi axiómára is,
értelemszerű
azonosító-módosításokkal … */
Megjegyzés: a további axiómák beillesztése semmi elvi gondot nem jelent, csak bántóan unalmas. Ezt a „gyakorlati” problémát ki lehet küszöbölni a kód a lényeget nem érintő átalakításával (néhány ismétlődő funkció önálló szabályba szervezésével, elkülönítésével). A B. függelék tartalmaz egy ilyen céllal módosított Prolog programot.
4. A puding próbája
Lefuttatva az így megtervezett és kódolt Prolog programot némi csalódást hozott az eredmény. L. a 4.1. ábrát!
|
|
|
4.1. ábra – futási eredmény |
Mint látható, az első axióma második tesztesete (tudniillik: nem üres, definiált, azaz legális állapotban levő veremre alkalmazva) hamis eredményre vezetett! Elemezve az axióma meglehetősen rövid szövegét, és belegondolva mondanivalójába, rájöhetünk: az axióma nem „teljes”. Állítása, hogy „Üres?(Üres)”, nem fejezi ki azt, mi legyen az Üres? függvény válasza a nem 0 elemet tartalmazó verem esetén.
Fogtunk tehát egy hibát? Nem! Az axiómarendszer nem hibás, hiszen a „nem üres verem” esetével a 2. axióma foglalkozik. Az persze kétségtelen, hogy az érintett axióma önmagában nem „teljes”. Ha el akarjuk kerülni a teszt szigorú „kritikáját”, módosítanunk kell az 1. axiómát: „v=Üres Û Üres?(v)”. A kódmódosítás a Clauses részt érinti. A meglévő „legális” adatra vonatkozó igaz-értékű kijelentés az üres veremre alkalmazható. Mondjuk ki tehát, hogy a nem üres veremre az Üres? függvény hamissal válaszol:
Clauses
…
axioma1(V,igaz) if
axioma1_1(V,igaz).
axioma1(V,igaz)
if
axioma1_2(V,igaz).
axioma1(verem(_,nemDef),igaz).
axioma1(_,hamis).
axioma1_1(V,igaz) if
ures(V) and uresE(V,igaz).
axioma1_2(V,igaz) if
not(ures(V)) and
not(uresE(V,igaz)).
…
|
|
|
4.2. ábra – futási eredmény |
Ez rávilágít arra, hogy számítani kell olyan axiómarendszerre is, amelynél több axióma fogalmaz meg egy, a tesztelési filozófiánk szempontjából egybe tartozó állítást. Az ilyenkor kijövő „kritika” nem jelent feltétlen hibát. Külön vizsgálatot igényel.
Tipikusabb hiba az, amikor egy operátor előfeltétel hiányos. Idézzük elő ezt úgy, hogy pl. a Tető operátor előfeltételét egyszerűen kihagyjuk. [Pr2]
|
|
|
4.3. ábra – futási eredmény |
A módszer megnyugtatóan szigorúnak (talán túlzottan is szigorúnak?!?) mutatkozott.
Hasznos további kísérletnek látszik a veremmel kapcsolatban kimondani állításokat, s ellenőrizni őket a program definiálta verem-szabályok terében. Lássunk erre is egy példát! [Pr3]
A verem egy jól ismert tulajdonságát fogalmazhatjuk meg a következő tétellel: „A verem egy LIFO szerkezet”. Ezt így formalizálhatjuk:
"nÎN : ( v0=Üres
Ù
"iÎ[1..n]
: vi=Verembe(vi-1,i) Ù
wn=vn Ù
"kÎ[1..n]
: ( Veremből(wn-k+1)=(wn-k,en-k+1)
Ù
en-k+1=n-k+1 ) )
A „bizonyítás” a következő:
1. Töltsük föl a vermet 1..N számokkal, i. elemének az értéke legyen i, tehát egyezzen meg a betétel sorszámával, az időrend könnyű ellenőrzése kedvéért.
2. Vegyük ki belőle az elemeket, és ellenőrizzük, hogy a k.-ként kivett az N–k+1.-ként betett elem-e (vagyis az N–k+1 értékű), épp ez jelenti a bizonyítandó fordított sorrendet!
Az előbbiekben felépített program kisebb módosításával kaphatjuk a megoldó programot. A Prolog axiómák és szabályok közül kihagyhatók azok, amelyek az algebrai specifikációhoz tartoznak, a Goal rész teljesen kicserélődik.
…
Predicates
…
ellenoriz(TVeremK,Integer)
letrehoz(TVeremK,Integer)
allitas(Integer)
Clauses
…
allitas(N) if
letrehoz(V,N) /*(1,2,..,N) verem
létrehozása*/ and
ellenoriz(V,N) /*(N,...,2,1)
sorrendben vehetők ki az elemek*/.
letrehoz(V,0) if
ures(V).
letrehoz(V,N) if
N-1=N1 and letrehoz(V1,N1) and
verembe(V1,N,V).
ellenoriz(_,0).
ellenoriz(V,N) if
N-1=N1 and verembol(V,E,V1) and E=N and
ellenoriz(V1,N1).
Goal
clearwindow and N=… ide irandó a veremhossz … and
allitas(N) and
Write("Állitás igaz
",N,"-elemű veremre.") and nl
Mivel
esetleges hibák kimutatása a cél, jobb felkészülni a program komolyabb
eltévelyedéseire:
1.
valamilyen
illeszkedési gond miatti „végtelen” keresési ciklusba esés,
2.
nemdefiniált
érték váratlan kijövetele.
Ezekre a hibalehetőségekre gondolva „bonyolítjuk” a programunk
szabályait eképpen. (A kód módosításait kiemeltük.)
…
allitas(N) if
letrehoz(V,N) /*(1,2,..,N) verem
létrehozása*/ and
! and
/*az előzőn túljutva visszalépésnek nincs értelme*/
write(V) and nl and
V=verem(_,def) /*nem volt illegális
művelet*/ and
! and /*az eddigieken
túljutva visszalépésnek nincs értelme*/
ellenoriz(V,N)
/*(N,...,2,1) sorrendben vehetők ki az elemek*/.
…
letrehoz(V,N) if
N-1=N1 and N1>=0 and
letrehoz(V1,N1) and verembe(V1,N,V) and
V=verem(_,def) /*nem volt illegális művelet*/
or
write("Hiba a
generáláskor.") and nl and fail.
…
ellenoriz(V,N) if
N-1=N1 and N1>=0 and
verembol(V,E,V1) and E=N and
ellenoriz(V1,N1) and
V=verem(_,def) /*nem volt illegális művelet*/
or
write("Hiba az
ellenőrzéskor.") and nl and fail.
Az állítás szabály nyomkövetését segíti csak
a középtájon elhelyezett write operátor; lényegibb közlendője van a létrehoz és az ellenőriz szabályokban elhelyezett kiírásoknak: „Hiba … !”. A hiba-ágak
végén található Fail a
szabály nem teljesülését erőszakolja ki, így gátoljuk meg a futás
értelmetlen folytatását. Ezt figyelhetjük meg az alábbi szándékosan elrontott
specifikáció esetén. A hiba: a Verembe operátor duplán helyezi be az elemet, ezzel elrontja az elemek
várt egymásrakövetkezését:
verembe(verem(V,def),E,verem([E,E|V],def)).
A program jelzését mutatja a 4.4. ábra.
|
|
|
4.4. ábra – futási eredmény |
Megjegyzés:
a hibajelzés duplázódásának az az oka, hogy az elsőként kivett számot (5) jónak
találta („…
verembol(V,E,V1) and E=N …”, E is, N is 5), s továbbhaladva a
következőnél (a 4 helyett 5-öt találva; N=4, E=5) akadt el. Így ezt is, meg
visszalépve az előzőhöz, azt is el kellett vetnie („! and write … and fail”). Vegyük észre, hogy valójában
felesleges a „hiba-ágban” a vágás, hiszen sem a létrehoz, sem az ellenőriz szabályoknak nincs más
alternatívája, amihez mintaillesztés ürügyén visszatérhetne a Prolog program. [Pr4]
5. Összefoglalás
A módszerre visszatekintünk, és röviden összefoglaljuk, hogy a kétféle specifikáció kellékeit hogyan egyesítjük egyetlen Prolog programban.
4.1. Az operációk szabályalakja (Domains/Predicates)
Operátor(Értelmezési tartomány): Értékkészlet
Prolog párja:
Operátor(Értelmezési tartomány , Értékkészlet)
szignatúrájú szabály lesz.
Mind az értelmezési tartományt, mind az értékkészletet, ha halmazok direktszorzatából tevődik össze, akkor paraméterek listájával írjuk le. A „fő” paraméter (azaz a vizsgált struktúra) helyére, a definiáltságot is tartalmazó kibővített típust kell, írjuk. (Konstruktor és destruktor esetén az egyik paraméter –értelemszerűen– elmarad.)
A Prolog program ezek után fixálódott deklarációs része az alábbi lesz, amelyben típustól (osztálytól) függően mindössze a TElem típus marad kitöltendő, és természetesen az operátorok szignatúrái. (A változó részeket kiemeltük.) Látható, hogy bizonyos nyelvi-kódolási konvenciókat követünk:
· Típusok neve „T”-vel kezdődik.
· A Prolog kódolás kedvéért „bővített” struktúra neve az „absztrakt” neve + „K”.
Domains
TElem = ??
/*
generic-paraméter */
TNemDef = nemDef; def
TStruktura = TElem*
TStrukturaK =
sruktura(TStruktura,TNemDef)
TLogikai = igaz; hamis
Predicates
Op1(TStrukturaK … /* input paraméterek */,
TStrukturaK … /* output paraméterek
*/)[14]
…
4.2. Az operátorok P/P-specifikációjának szabálymegfelelője (Clauses)
A Prolog Clauses részbe kerülnek az operátorok szabályai. Elsőként a rávonatkozó implicit error-axióma megfelelőjét kell megfogalmazni, majd PP-specifikációt öntjük Prolog szabály alakjába; ha a használatkor hiba-állapotba (nemDef) jut a struktúra, akkor ehhez is tartozik szabály.
Ha az operátor működése során a struktúra állapotát nem módosítja (az ilyeneknek az export modulban is függvényt feleltetünk meg), akkor
Clauses
…
/* Implicit error-exióma: */
Op1(struktura(_,nemDef),
/* input struktúraparaméter: „szabad” */
_, … , /* további input paraméterek */
_, … ). /* output paraméterek
„szabadok” */
/* PP-specifikáció: */
Op1(struktura(ST,def),
/* input struktúraparaméter */
_, … , /* további input paraméterek */
_, … ). /* output paraméterek */
…
Ha az operátor paraméterlistáján mind input, mind output szerepben felbukkan a struktúra paraméter (ezek szerepelnek az export modulban eljárásként), akkor
…
/* Implicit error-exióma: */
Opi(struktura(ST,nemDef),
/* input struktúraparaméter */
_, … , /* további input paraméterek „szabadok” */
struktura(ST,nemDef),
/* output struktúraparaméter: változatlan */
_, … ). /* további output
paraméterek „szabadok”
*/
/*
PP-specifikáció: */
Opi(struktura(STi,nemDef),
/* input struktúraparaméter */
_, … , /* további input paraméterek */
struktura(STo,nemDef),
/* output struktúraparaméter */
_, … ). /* további output
paraméterek */
/* esetleg,
PP-specifikáció: hiba-állapotba jutás */
Op1(struktura(ST,def), /* input struktúraparaméter */
_, … , /* további input paraméterek */
struktura(ST,nemDef), /* output struktúraparaméter: változatlan;
állapotváltozás: def®nemDef */
_, … ). /* további output
paraméterek „szabadok”
*/
Vegyük észre, minden operátorhoz legalább két Prolog szabály tartozik.
4.3. Az algebrai axiómák mint szabályok (Predicates/Clauses)
Az axiómák szignatúráját először a Prolog Predicates részében kell definiálni:
Predicates
Ax1(TStrukturaK /*a fő struktúra*/,TLogikai /*teljesül-e*/)
…
Majd az összefüggést a Clauses részben helyezzük el, átültetve a formálisan megadott axiómát:
Clauses
…
Ax1(TSk /*fő típus*/, IVN /*igen vagy nem*/) if
… a
formális axióma kódja, a szereplő függvények Prolog függvényes
párjának hívásával …
Ax1(_,hamis). /* minden egyéb esetre hamis */
…
Vegyük észre, minden axiómához legalább két Prolog szabály tartozik.
4.4. Az összeillés vizsgálatának kezdeményezése (Goal)
A tényleges ellenőrzést „kiváltó” célállítást minden axiómára külön-külön két esetre kell megfogalmazni:
· az üres (és definiált) struktúrára,
·
a nem üres (és definiált) struktúrára:
Goal
clearwindow and
/*(üres,def)-re igaz-e:*/
ST0=struktura([],def) and
ax1(ST0,JoE0) and
write("1:",JoE0) and
write(" ",ST0,"-re") and nl
and ! /*a visszalépés értelmetlen*/ and
/*(nem üres,def)-re igaz-e:*/
ST=struktura([_],def) and
ax1(ST,JoE) and
write("1:",JoE) and
write(" ",ST,"-re.") and nl
and ! /*a visszalépés értelmetlen*/ and
… /* … és a többi
axiómára is … */
Irodalom
Kozma L. – Varga L.: „Adattípusok osztálya.”, ELTE TTK Informatikai TanszékCsoport, 2001
Fekete I. – Hunyadvári L.: „Az adattípus absztrakciós szintjei”, Informatika a felsőoktatásban’99 konferencia, Debrecen, 2002
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
N. Gehani –
A.D.McGettrich: „Software Specification Techniques.”, Addison-Wesley, 1986
Szlávi P. – Zsakó L.: „Módszeres programozás – Gráfok, gráfalgoritmusok.”, ELTE TTK Informatikai TanszékCsoport, 2000
Szlávi P.: „Programok, programspecifikációk.”, Informatika a felsőoktatásban’99 konferencia, Debrecen, 1999
Rich,K.–Robinson,Ph.: „Using Turbo Prolog.”, Borland-Osborne/McGraw-Hill, 1988
Programhivatkozások
Szlávi P.: „A verem
specifikációinak kompatibilitását ellenőrző Prolog program.”, http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/VEREM4.PRO
Szlávi P.: „A verem
specifikációinak kompatibilitását ellenőrző Prolog program – hibás
P/P-specifikációval.”, http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/VEREM4H2.PRO
Szlávi P.: „A verem
specifikációinak kompatibilitását ellenőrző Prolog program – egy állítás ellenőrzése.”,.
http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/VEREMALL.PRO
Szlávi P.: „A verem
specifikációinak kompatibilitását ellenőrző Prolog program – egy állítás
ellenőrzése, hibás P/P-specifikáció mellett.”, http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/VEREMALH.PRO
Függelék
A. Sorozat betét
Az alábbi kóddal a lényeget igyekszünk kifejezni. A külön „Sorozat.inc” file-ba kiemelt kódot az include „Sorozat.inc” Prolog utasítással illeszthetjük a mindenkori programunkhoz.
Domains
TSorozat = TElem*
Predicates
% a sorozatnak elem-e az
adottadik:
eleme(TSorozat, Integer /*dik*/,
TElem, TLogikai)
% a sorozatnak hossza:
hossz(TSorozat, Integer)
% a két sorozat elemei azonosak-e az
adott sorszámig:
azonos(TSorozat,
TSorozat, Integer /*ig*/)
…
Clauses
eleme([],_,_,hamis).
eleme([E|_],1,E,igaz).
eleme([_|S],I,EE,igaz) if
II=I-1 and I>1 and
eleme(S,II,EE,igaz).
hossz([],0).
hossz([_|S],H) if
hossz(S,HH) and H=HH+1.
azonos(_,_,0).
azonos([E|S],[E|T],H) if
HH=H-1 and azonos(S,T).
…
B. Módosított Prolog program
Kiemeléssel jeleztük az eltérést. [Pr1]
Domains
TNemDef = nemDef; def
TElem = Integer
TVerem = TElem*
TVeremK = verem(TVerem,TNemDef)
TLogikai = igaz; hamis
Predicates
ures(TVeremK)
uresE(TVeremK /*input*/,
TLogikai /*output*/)
teto(TVeremK, /*input*/
TElem,TVeremK /*output*/)
verembe(TVeremK,TElem, /*input*/
TVeremK /*output*/)
verembol(TVeremK, /*input*/
TElem,TVeremK /*output*/)
axioma1(TVeremK,TLogikai /* teljesül-e */)
axioma1_1(TVeremK,TLogikai /*
teljesül-e */)
axioma1_2(TVeremK,TLogikai /*
teljesül-e */)
axioma2(TVeremK,TLogikai /* teljesül-e
*/)
axioma2_1(TVeremK,TLogikai /*
teljesül-e */)
axioma3(TVeremK,TLogikai /* teljesül-e
*/)
axioma3_1(TVeremK,TLogikai /*
teljesül-e */)
axioma3H(TVeremK,TLogikai /*
teljesül-e */) /* hiba-axióma */
axioma3H_1(TVeremK,TLogikai /*
teljesül-e */)
axioma4(TVeremK,TLogikai /* teljesül-e
*/)
axioma4_1(TVeremK,TLogikai /*
teljesül-e */)
axioma4_2(TVeremK,TLogikai /*
teljesül-e */)
axioma4H(TVeremK,TLogikai /*
teljesül-e */) /* hiba-axióma */
axioma4H_1(TVeremK,TLogikai /*
teljesül-e */)
ellenorzes1(TVeremK)
ellenorzes2(TVeremK)
ellenorzes3(TVeremK)
ellenorzes3H(TVeremK)
ellenorzes4(TVeremK)
ellenorzes4H(TVeremK)
Clauses
ures(verem([],def)).
uresE(verem(_,nemDef),_). /* ImpErrAx
*/
uresE(verem([],def),igaz).
uresE(verem([_],def),hamis).
uresE(verem([_|_],def),hamis).
teto(verem(V,nemDef),_,verem(V,nemDef)). /*
ImpErrAx */
teto(verem([E|V],def),E,verem([E|V],def)). /* PP */
teto(verem([],def),_,verem([],nemDef)). /* PP: Err */
verembe(verem(V,nemDef),_,verem(V,nemDef)).
/* ImpErrAx */
verembe(verem(V,def),E,verem([E|V],def)). /* PP */
verembol(verem(V,nemDef),_,verem(V,nemDef)).
/* ImpErrAx */
verembol(verem([E|V],def),E,verem(V,def)). /* PP */
verembol(verem([],def),_,verem(_,nemDef)). /* PP: Err */
axioma1(V,igaz) if
axioma1_1(V,igaz).
axioma1(V,igaz) if
axioma1_2(V,igaz).
axioma1(_,hamis).
axioma1_1(V,igaz) if
ures(V) and uresE(V,igaz).
axioma1_2(V,igaz) if
not(ures(V)) and
not(uresE(V,igaz)).
axioma2(V,igaz)if
axioma2_1(V,igaz).
axioma2(_,hamis).
axioma2(V,igaz) if
verembe(V,_,verem(W,def)) and !
and
uresE(verem(W,def),hamis).
axioma3(V,igaz)if
axioma3_1(V,igaz).
axioma3(_,hamis).
axioma3_1(V,igaz) if
verembe(V,E,W) and ! and
teto(W,E,W)
axioma3H(verem(_,def),igaz)if
axioma3H_1(verem(_,def),igaz).
axioma4H(_,hamis).
axioma3H_1(verem(_,def),igaz) if
uresE(verem(_,def),igaz) and
! and
teto(verem(_,def),_,verem(_,nemDef)
or
uresE(_,hamis).
axioma4(V,igaz) if
axioma4_1(V,igaz) and
axioma4_2(V,igaz).
axioma4(_,hamis).
axioma4_1(V,igaz) if
verembe(V,E,W) and ! and
verembol(W,E,V).
axioma4_2(V,igaz) if
uresE(V,hamis) and ! and
verembol(V,E,W) and ! and verembe(W,E,V)
or
uresE(V,igaz).
axioma4H(verem(_,def),igaz) if
axioma4H_1(verem(_,def),igaz).
axioma4H(_,hamis).
axioma4H_1(verem(_,def),igaz) if
uresE(verem(_,def),igaz) and
! and
verembol(verem(_,def),_,verem(_,nemDef)
or
uresE(_,hamis).
ellenorzes1(Teszt) if
write("1:'",Teszt,"'-re") and
axioma1(Teszt,JoE) and
write("?: ",JoE) and
nl.
ellenorzes2(Teszt) if
write("2:'",Teszt,"'-re") and
axioma2(Teszt,JoE) and
write("?: ",JoE) and
nl.
ellenorzes3(Teszt) if
write("3:'",Teszt,"'-re") and
axioma3(Teszt,JoE) and
write("?: ",JoE) and
nl.
ellenorzes4(Teszt) if
write("4:'",Teszt,"'-re") and
axioma4(Teszt,JoE) and
write("?: ",JoE) and
nl.
ellenorzes4H(Teszt) if
write("4H:'",Teszt,"'-re") and
axioma4H(Teszt,JoE) and
write("?: ",JoE) and
nl.
Goal
clearwindow and
/* 1. axióma tesztje: */
/*(üres,def)-re igaz-e:*/
V01=verem([],def) and ellenorzes1(V01)
and
/*(nem üres,def)-re igaz-e:*/
V1=verem([_],def) and ellenorzes1(V1)
and ! and /* 2. axióma tesztje:
*/
/*(üres,def)-re igaz-e:*/
V02=verem([],def) and ellenorzes2(V02)
and
/*(nem üres,def)-re igaz-e:*/
V2=verem([_],def) and ellenorzes2(V2)
and ! and /* 3. axióma tesztje:
*/
/*(üres,def)-re igaz-e:*/
V03=verem([],def) and ellenorzes3(V03)
and
/*(nem üres,def)-re igaz-e:*/
V3=verem([_],def) and ellenorzes3(V3)
and ! and /* 4. axióma tesztje:
*/
/*(üres,def)-re igaz-e:*/
V04=verem([],def)
and ellenorzes4(V04)
and
/*(nem üres,def)-re igaz-e:*/
V4=verem([_],def) and ellenorzes4(V4)
and ! and /* 4H. axióma
tesztje: */
/*(üres,def)-re igaz-e:*/
V04H=verem([],def) and ellenorzes4H(V04H)
and
/*(nem üres,def)-re igaz-e:*/
V4H=verem([_],def)
and ellenorzes4H(V4H)