0. Bevezetés
A módszer eddig jól vizsgázott. Ha alkalmazzuk más típusosztály specifikációinak kompatibilitás vizsgálatára, kiderül, hogy valóban szélesebb körben is alkalmazható-e. Erre vagyunk kíváncsiak ebben a részben.
Rájövünk majd, hogy bár nincs elvi kifogás a módszerrel szemben, de az eleganciában hagy maga után kívánni valót. S ez ok lesz majd arra, hogy finomítsuk.
A programozásban az elegancia nem valamiféle hanyagolható külcsín, „úri huncutság”, hanem a biztonságosság egyik tipikus velejárója, talán nem túlzás állítani: záloga. Ami elegáns, az tetszetős, az könnyen áttekinthető, a helyessége könnyűszerrel belátható. Vagyis a biztonságosság és az elegancia lényegi, tartalmi kapcsolatban állnak egymással.
1. A probléma forrása
A problémát közelítsük meg egy másik típusosztály, a sor példáján keresztül! Mindenek előtt lássuk e típusosztály kétféle specifikációját! [SzP1999]
1.1. A sor algebrai specifikációja
|
|
Sor(Típus Elem): Asszociált műveletek: Üres:
Sor Üres?(Sor):
Logikai
Első(Sor):
Elem È {NemDef} Sorba(Sor,Elem):
Sor È {NemDef} Sorból(Sor):
( Sor x Elem ) È {NemDef} Axiómák: Jelölések: · s,s’: Sor(Elem) = Sortípusú objektum · e,e’: Elem = elemtípusú
objektum 1o Üres –
axióma s=Üres Û Üres?( s) 2o Üres? – axióma Ø Üres?(Sorba(s,e)) 3o Első–Sorba
– axióma Üres?(s) Þ
Első(Sorba(s,e))=e Ù 3’o Első –
hiba-axióma Üres?(s) Þ Első(s)=NemDef 4o
Sorból–Sorba – axióma Üres?(s) Þ Sorból(Sorba(s,e))=(s,e) Ù 4’o Sorból –
hiba-axióma Üres?(s) Þ Sorból(s)=NemDef
|
1.2. A sor P/P-specifikációja
ExportModul Sor(Típus
ElemTip):
[Jelölések a specifikációhoz:
1) Sor = sorozat x hiba
2) s’ a Sor “új” állapota, ha a
korábbitól meg kell
különböztetni ]
Eljárás
Üres(Változó s:Sor)
[Sorlétrehozás
a memóriában]
Ef: Ø$sÎSor
Uf: $sÎSor Ù
s=((),Hamis)
Függvény
Üres?(Konstans
s:Sor): Logikai
[üres-e
a Sor]
Ef: $sÎSor Ù
Øs.hiba
Uf: Üres?(s)=(s.sorozat=())
Függvény
Első(Változó s:Sor):
ElemTip
[a
Sor első elemének értéke]
Ef: $sÎSor Ù
Øs.hiba
Uf: s.sorozat=(s1,...,sn)
Þ
Első(s)=s1
s.sorozat=() Þ
s’.hiba=Igaz
Eljárás
Sorba(Változó s:Sor, Konstans e:ElemTip)
[Sorbatétel]
Ef: $sÎSor Ù
Øs.hiba
Uf: s.sorozat=(s1,...,sn)
Þ
s’=((s1,...,sn,e),Hamis)
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
Hibás?(Változó
s:Sor): Logikai
[történt-e
hiba a Sorra hivatkozás
során, “törli” a hibaváltozót]
Ef: $sÎSor Ù
Øs.hiba
Uf: Hibás?(s)=s.hiba
Ù
s’.hiba=Hamis
Modul vége.
1.3. A kódolás első három lépése
Az I. részben részletezett módszer szerint járunk el az algebrai axiómák és a P/P-specifikációbeli állítások szabállyá alakításánál. A következő lépéseket kell megtennünk a sor fenti két specifikációja alapján:
1. a P/P-specifikációkból előállítjuk a megfelelő Prolog szabályokat, majd
2. az algebraiban szereplő axiómák átültetése következik (itt már ügyelünk a vágások helyes „beültetésére” is), utána
3. az ellenőrzést megszervező szabályokat alkotjuk meg, és végül
4. a célállítás létrehozásával zárjuk.
A 4. lépést későbbre hagyjuk. Alábbiakban különösebb kommentárok nélkül olvashatjuk a kód megfelelő, jellemző darabkáit. Észrevehetjük, hogy az I. rész B. függelékében szereplő kódot tekintjük kiindulási alapnak. Az elnevezésből adódó különbségekre, mint típusneveké (TVerem helyett TSor stb.), nem térünk ki. Ugyancsak elhagyjuk a mechanikusan képezhető ismétlődéseket. Most komoly szerep jut a sorozatkezelő „segédrutinoknak”, ezért azokkal kapcsolatos kódrészeket viszont feltüntetjük.
Abból adódóan, hogy a sor egyszerre két végén is „aktív” némi „bonyodalom” akad. Éppen ezen bonyodalmak megoldásában játszanak fontos szerepet a sorozatkezelő műveletek. Érdemes egy pillanatot időzni a sor szempontjából legdöntőbb művelethármas (Első, Sorba, Sorból) Prolog-beli megfogalmazásánál. A Prolog sorozatszervezés logikája miatt az egyik „vég” manipulálása egyszerű, a másik ellenben csak segédszabály, pl. az alábbi Eleme szabály útján végezhető. Ez a sorozat tetszőleges sorszámú elemét „éri el”:
|
a mintaprogram
részlete |
magyarázat |
|
eleme([],_,_,hamis). eleme([E|_],1,E,igaz). eleme([_|S],I,EE,igaz) if |
Üres sorozatban nincs sehányadik elem. Igaz, ha az 1. elem épp a kellő. Ha nem az 1. eleméről van szó, akkor a maradék sorozat eggyel kisebb indexű eleme kell legyen. |
Döntenünk kell arról, hogy a sorozat mely végén legyen a sor első eleme. Mivel ezt az elemet két sor-művelet is használja (Első, Sorból), ezért a Prolog szempontjából kényelmes megoldást választjuk: a fejnél kutakodnak.
|
elso(sor(S,nemDef),_,sor(S,nemDef)). elso(sor([E|S],def),E,sor([E|S],def)). elso(sor([],def),_,sor([],nemDef)). sorbol(sor(S,nemDef),_,sor(S,nemDef)). sorbol(sor([E|S],def),E,sor(S,def)). sorbol(sor([],def),_,sor(_,nemDef)). |
Az első művelet implicit error-axiómája. A sor első elem a sorozat feje. Üres sorra nem definiált a művelet. A sorból művelet implicit error-axiómája. A sor első elem a sorozat feje, kiveendő. Üres sorra nem definiált a művelet. |
A Sorba szabálya a sorozat nehezebben hozzáférhető utolsó elemét manipulálja. Ehhez már szükséges az eleme és egy eddig nem említett szabály (azonos) felhasználása.
|
sorba(sor(S,nemDef),_,sor(S,nemDef)). sorba(sor(S,def),E,sor(T,def))
if |
A sorba művelet implicit error-axiómája. A sorba betett elem –az időrend megérzése okán– éppen a sorszámával kell megegyezzék. Az előzőleg betett elemek nem változnak. Erre a szabályzáradékra csak azért van szükség, mert a Prolog különben képtelen lenne konkrét értékű sorozatokat előállítani. |
A felhasznált azonos szabály egy újabb sorozatkezelő operáció, amely akkor igaz, ha a két paramétersorozatának első valahány eleme megegyezik. Az ellenőrizendő elemek száma a harmadik paraméter.
|
azonos(_,_,0). |
Ha nincs mit ellenőrizni, akkor igaz. Ha a sorozatok fej-elemei azonosak, akkor a sorozatok maradék elemein múlik. |
Lássuk most már a programot egyben (a könnyen kitalálható részek nélkül):
Predicates
eleme(TSor,Integer,TElem,TLogikai)
hossz(TSor,Integer)
azonos(TSor,TSor,Integer /*ig*/)
ures(TSorK)
uresE(TSorK
/*input*/,
TLogikai
/*output*/)
elso(TSorK,
/*input*/
TElem,TSorK
/*output*/)
sorba(TSorK,TElem,
/*input*/
TSorK
/*output*/)
sorbol(TSorK,
/*input*/
TElem,TSorK
/*output*/)
axioma1(TSorK,TLogikai /* teljesül-e
*/)
…
ellenorzes1(TSorK)
…
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).
ures(sor([],def)).
uresE(sor(_,nemDef),_). /* ImpErrAx */
uresE(sor([],def),igaz).
uresE(sor([_],def),hamis).
uresE(sor([_|_],def),hamis).
elso(sor(S,nemDef),_,sor(S,nemDef)). /*
ImpErrAx */
elso(sor([E|S],def),E,sor([E|S],def)).
/* PP */
elso(sor([],def),_,sor([],nemDef)). /*
PP: Err */
sorba(sor(S,nemDef),_,sor(S,nemDef)). /*
ImpErrAx */
sorba(sor(S,def),E,sor(T,def)) if /*
PP */
hossz(S,N) and N1=N+1 and
hossz(T,N1) and
eleme(T,N1,E,igaz) and
azonos(S,T,N).
sorbol(sor(S,nemDef),_,sor(S,nemDef)). /*
ImpErrAx */
sorbol(sor([E|S],def),E,sor(S,def)).
/* PP */
sorbol(sor([],def),_,sor(_,nemDef)). /* PP: Err */
axioma1(S,igaz) if
axioma1_1(S,igaz).
axioma1(S,igaz)if
axioma1_2(S,igaz).
axioma1(_,hamis).
axioma1_1(S,igaz) if
ures(S) and
uresE(S,igaz).
axioma1_2(S,igaz) if
not(ures(S)) and
not(uresE(S,igaz)).
axioma2(S,igaz) if
axioma2_1(S,igaz).
axioma2(_,hamis).
axioma2_1(S,igaz) if
sorba(S,_,sor(T,def)) and
! and
uresE(sor(T,def),hamis).
axioma3(S,igaz) if
axioma3_1(S,igaz).
axioma3(_,hamis).
axioma3_1(S,igaz) if
uresE(S,igaz) and ! and
sorba(S,E,T) and ! and
elso(T,E,T)
or
uresE(S,hamis).
axioma3H(sor(_,def),igaz) if
axioma3H_1(sor(_,def),igaz).
axioma3H(_,hamis).
axioma3H_1(sor(_,def),igaz) if
uresE(sor(_,def),igaz) and
! and
elso(sor(_,def),_,sor(_,nemDef))
or
uresE(sor(_,def),hamis).
axioma4(S,igaz) if
axioma4_1(S,igaz) and
axioma4_2(S,igaz).
axioma4(_,hamis).
axioma4_1(S,igaz) if
uresE(S,igaz) and ! and
sorba(S,E,T) and ! and
sorbol(T,E,S)
or
uresE(S,hamis).
axioma4_2(S,igaz) if
uresE(S,hamis) and ! and
sorbol(S,E1,T1) and ! and
elso(S,E2,S) and E1=E2
and ! and
sorba(T1,E4,T2) and ! and
sorba(S,E4,T3) and ! and
sorbol(T3,_,T4) and T2=T4
or
uresE(V,igaz).
axioma4H(sor(_,def),igaz) if
axioma4H_1(sor(_,def),igaz).
axioma4H(_,hamis).
axioma4H_1(sor(_,def),igaz) if
uresE(sor(_,def),igaz) and
! and
sorbol(sor(_,def),_,sor(_,nemDef)).
or
uresE(sor(_,def),hamis).
ellenorzes1(Teszt) if
write(„1:’”,Teszt,”’-re”) and
axioma1(Teszt,JoE) and
write(„?: „,JoE) and nl.
…
1.4. A szabályok programmá egyesítése
A negyedik lépés következik. A verem esetén 2 „mintastruktúrára” volt szükség a „teszteléshez”, nevezetesen, amelynél a verem állapota „definiált” volt és:
1. elemeinek sorozata üres,
2. tartalmaz legalább egy elemet.
Kérdés: a sor esetén is éppen ez a két szignifikáns eset van-e. Vegyük észre, hogy míg a veremnek, mint sorozatnak, egyetlen „aktív” vége van, addig a sornak kettő. Ekkor viszont nyilvánvalóan nem azonos kategóriába sorolandó a pontosan egy elemű sorozat esete, mint a kettő, vagy annál több. Egyetlen elem esetén a sorozat eltérő végére vonatkozó műveletek ugyanazt az elemet érintik, a kettő (vagy több) elem esetén már nem.
A probléma tehát az, hogyan dönthető el biztonságosan:
mely mintastruktúrákra (jelen esetben sorozatra) kell a
kompatibilitást ellenőrizni?
2. A probléma megoldása
Jogosnak látszik egy újabb esettel bővíteni mintastruktúrák halmazát; nevezetesen azzal, amelyben a sorozatnak különválik a két „aktív” vége, azaz a (legalább) kételemű sorozattal:
3. A verem (definiált értékű, és) legalább két elemet tartalmaz.
Általános elvként fogalmazhatjuk meg, hogy a sorozatok „külön életet élő”, vagyis csak rájuk vonatkozó művelettel rendelkező elemeihez, külön tesztet kell szentelni. A tömb esetén, pl. N-t, ha N-elemű a tömb.
A sor célállításbeli formuláját ebben a szellemben képezzük. Az alábbi kódrészletben kiemeltük az „újdonságokat”. [SorPr1]
…
Goal
clearwindow and
/*
1. axióma tesztje: */
/*(üres,def)-re igaz-e:*/
V0d1=sor([],def) and
ellenorzes1(V0d1)
and
/*(1-elemű,def)-re igaz-e:*/
V1d1=sor([1],def) and
ellenorzes1(V1d1)
and
/*(legalább 2-elemű,def)-re igaz-e:*/
V2d1=sor([1|_],def) and
ellenorzes1(V2d1)
and
…
A futás eredményével elégedettek lehetünk. A kompatibilitást teljesnek állítja a program. (L. a 2.1. ábrát!)
|
|
|
2.1. ábra – futási eredmény |
„Mesterséges” hibákra is jól reagált, amint az alábbi példák bizonyítják. Az elkövetett hibák a következők voltak:
1. Az Első művelet a Sorból mintájára, nemcsak kiolvassa a sorbeli első értéket, hanem azt –tévesen– ki is veszi: „elso(sor([E|S],def),E,sor(S,def))”. (L. 2.2. ábra! [SorPr2])
2. A Sorból művelet az Első-höz hasonlóan, bennhagyja az első elemet, ahelyett, hogy megszüntetné azt: „sorbol(sor([E|S],def),E,sor([E|S],def))”. (L. 2.3. ábra! [SorPr3])
3. A Sorból művelet üres sorra alkalmazva, hibásan, def állapotban „felejti” a sort; s így nem jelzi a reá nézve inkorrekt használatot: „sorbol(sor([],def),_, sor(_,def))”. (L. 2.4. ábra! [SorPr4])
|
2.2.
ábra – futási eredmény |
|
2.3.
ábra – futási eredmény |
|
2.4. ábra – futási eredmény |
Ahogy az I. részben a verem LIFO-ság tulajdonság vizsgálatát végeztük, lássuk be most a sor FIFO-ságát! A sor e tulajdonságát így formalizálhatjuk:
"nÎN : ( s0=Üres
Ù
"iÎ[1..n]
: si=Sorba(si-1,i) Ù
ssn=sn
Ù
"kÎ[1..n]
: ( Sorból(ssn-k+1)=(ssn-k,ek)
Ù
ek=k
) )
A „bizonyítás” menete megegyezik az I. részben taglalttal;
az eltérések pedig a sor-verem cseréből értelemszerűen fakadnak. A „bizonyítás”
lényegét felidézzük:
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 a k.-ként betett elem-e (vagyis a k értékű), épp ez jelenti a bizonyítandó egyenes sorrendet!
Meglepő, hogy az „egyenes” sorrend ellenőrzése bonyolultabb, mint a fordítotté. Ui. a korábbi gondolatmenet értelében az ellenőrzést végző szabály rekurzívan visszafelé haladva a sorozat i. elemét az N–i. lépésben éri el, ahol N-nel jelöltük a sorozat „eredeti” hosszát. Vagyis ahhoz, hogy a várt elem értékét ellenőrizhessük nem elegendő a sorozat aktuális –még feldolgozandó– hosszát tudni, kell a kiinduló hosszat is. Ez magyarázza a többletparamétert:
|
a mintaprogram
részlete |
magyarázat |
|
ellenoriz(_,0,_). ellenoriz(S,N,NN)
if S=sor(_,def) or write("Hiba az ellenőrzéskor.") and
|
0-hosszú sorozatra nincs mit ellenőrizni. Az eredetileg NN-hosszú sorozat N-hosszúságú S „farka”, akkor megfelelő, ha első eleme éppen NN–N+1 értékű és sorból kivéve a maradék sor is ugyanezen értelemben helyes. A legálisan végrehajtható volta is a helyesség része. Ha bármely ok miatt nem volt teljesíthető a fenti szabály, akkor hiba hibaüzenettel. |
A FIFO-ságot ellenőrző program állítás-specifikus részét ideillesztjük, most már magyarázat nélkül:
… sor P/P-szabályok …
% az állítás ellenőrzése:
allitas(N) If
letrehoz(S,N) /*(1,2,...,N) sor létrehozása*/ and
! and /*visszalépésnek nincs értelme*/
write(S) and nl and
S=sor(_,def) /*a végrehajtás során
nem lett illegális művelet
végrehajtva*/ and
! and /*visszalépésnek nincs értelme*/
ellenoriz(S,N,N) /*(1,2,..,N)
sorrendben vehetők ki az elemek*/.
letrehoz(S,0) If
ures(S).
letrehoz(S,N) If
N-1=N1 and N1>=0 and
letrehoz(S1,N1) and sorba(S1,N,S) and
S=sor(_,def) /*a végrehajtás során
nem lett illegális művelet
végrehajtva*/
or
write("Hiba a
generáláskor.") and nl and fail.
ellenoriz(_,0,_).
ellenoriz(S,N,NN) If
N-1=N1 and N1>=0 and
sorbol(S,E,S1) and E=NN-N+1 and
ellenoriz(S1,N1,NN) and
S=sor(_,def) /*a végrehajtás során
nem lett illegális művelet
végrehajtva*/
or
write("Hiba az
ellenőrzéskor.") and nl and fail.
Goal
… célállítás …
A fenti [SorAll] program futását N=5-re mutatja a 2.5. ábra.
3. Strukturális indukció alapú megoldás
El kell ismernem: az iménti megoldással –a jó futása ellenére– nem vagyok teljesen elégedett. Egyáltalán nem tűnik elegánsnak. Fölvetődik a kérdés, újabb meg újabb típus esetén mennyi elemszámú sorozattal kell tesztelni? Honnan lehet ezt kitalálni? Nagy az emberben a félsz, nem hagy-e számításon kívül valamilyen fontos esetet, s így egy esetleges hibát felfedetlenül.
Erre a problémára jelentene gyógyírt a strukturális indukció, melynek lényege a következő.
3.1. Strukturális indukció
Egy sorozattípus (jobban mondva: minden hozzátartozó értéke) akkor rendelkezik valamely adott T tulajdonsággal, ha rendelkezik az üres (vagy bármely adott számú elemet tartalmazó) sorozata azzal (T(( )) vagy T((s1, …,sK)) valamely rögzített K-ra); továbbá bizonyítható, hogy bármely N-elemű sorozatához újabb elemet hozzávéve az így nyert N+1-elemű sorozat megtartja a T-tulajdonságot.[2]
3.2. Strukturális indukció a kompatibilitás szolgálatában
Igazítsuk a strukturális indukció gondolatát jelen problémánkhoz: a kompatibilitás problémájához! Ötletünk a következő: lássuk be üres sorozatra minden egyes axióma teljesülését a P/P-specifikációk mellett, majd bizonyítsuk be, hogy ha feltesszük N-elemszámú sorozatra a kompatibilitás teljesülésülését, akkor eggyel több elemre is teljesül.
A gondolatmenet épít a korábbi módszer legtöbb elképzelésére. Ahol biztosan eltér: a kompatibilitás ellenőrzésének megszervezésében.
Az elképzelés vázlatát a verem 4º axiómáján mutatjuk be. Sarkalatos pontja, hogy olyan axiómát (vagy axiómát már egy vizsgált paraméter mellett) nem ellenőriz, aminek helyességét már korábban belátta. Ehhez fogjuk felhasználni a Prolog program adatbázis-kezelő szolgáltatásait: felvenni egy tényállítást az adatbázisba (assert), lekérdezni egy tényállítás bennlétét (a lekérdezett tényállítás maga).
Egy típus-axiómáról tudjuk vagy feltesszük teljesülését, akkor azt az egy adatbázisbeli szabály rögzíti: a készAxiomaOK(?,??) azt állítja, hogy a ? típus-axióma „rendben van” legfeljebb ??-hosszúságú sorozatokra.
Az elemzett program már tartalmazza –éppúgy, mint eddig– a P/P- és algebrai specifikációk szabályait. Ezt már nem részletezzük. Hívjuk axiomaOK4-nek a 4º axióma problémamentességét ellenőrző szabályt. Paramétere a sorozathossz, azé a sorozaté, amelyig igaz-teljesülését belátni óhajtjuk:
|
a mintaprogram
részlete |
magyarázat |
|
axiomaOK4(X) if |
Bizonyított-e a legfeljebb adott elemszámú sorozatra a 4º axióma? |
|
axiomaOK4(0)
if |
0 db elemre az axióma akkor igaz, ha az adott axióma teljesül az üres veremre. Teljesülésekor feljegyzendő. Ez játssza tehát a
strukturális indukció kiinduló feltételét. |
|
axiomaOK4(N)
if ! and
axioma4(verem([N|V],def),igaz) and |
Teljesül-e a 4º
axióma Majd hozzávéve az eggyel kisebb sorozathoz egy elemet, megmarad-e az axióma igaz volta? Ha igen, tényként feljegyezhető. Ez játssza a
bizonyításbeli indukció szerepét. |
|
axiomaOK4(N)
if |
Ha sehogyan sem sikerült belátni az axióma teljesülését, akkor a sikertelenség jelzése (képernyőre is). |
Megjegyzések: A vágás itt is az értelmetlen mintaillesztési kísérletek megakadályozását szolgálja. Ahogy ezt az I. részben láttuk, a helyes működéshez szükséges a „vágott” részeket al-szabályokba kiemelni. Ez itt is igaz; persze magától értetődő kivételekkel. Például nyilvánvalóan szükségtelen ez a bonyolítás csupán a jegyezdfelA szabály miatt, ami a bizonyított; így „axiómává” egyszerűsödött tényállításként veszi föl az adatbázisba. Itt tehát nem kell számolnunk a visszalépés „veszélyével”.
Az említett jegyezdfel szabály jól mutatja a Prolog adatbázis-kezelő szolgáltatásait. Pillantsunk rá a programunkra adatbázis-kezelés szempontjából!
|
Database
- axiomak |
Ez a deklaráció tudatja, hogy az „axiomak” nevű adatbázisba „keszAxiomaOK” nevű állítások kerülnek majd föl. |
|
jegyezdfelA(Ax,N)
if |
Már ismert-e az állítás (ez esetben nincs mit
tenni)? |
A bizonyítás megszervezése a következő szabályokkal történik:
|
bizonyit4(N)
if or |
Ha
már az üresre sem igaz, akkor a bizonyításnak vége (negatív üzenetet már
kiírtuk az axiomaOK4(0)-ban). Egyébként
(azaz az üresre igaz) a 0-eleműre ellenőrizni már nem kell, s rögzítjük az indukciós feltételt N-re, majd ellenőrizzük az axióma N-ről N+1-re következését. |
Ezután a program célállítás-része roppant egyszerűen alakul:
Goal
% inicializálás:
clearwindow and
% a kompatibilitás ellenőrzése strukturális indukcióval:
N=??? /*kitöltendő inputparaméter, ellenörzés nélkül*/ and
% 1. axióma:
bizonyit1(N) and !
/*a visszalépés értelmetlen*/ and
…
% 4H. axióma:
bizonyit4H(N)
Maradtak még tisztázatlan „részletkérdések”, amelyekre hamarosan visszatérünk. Figyeljük meg most a programot működés közben! [VerStin3]
|
|
|
3.1.
ábra – futási eredmény |
A futás N=5-re vonatkozik. Az ábra a működés mélyebb titkaiba enged bepillantást. Az eddigiek alapján az „AxOK?(??)”-szerű kiírások kitalálhatóak. (A „?” jelek valamilyen számjegyet helyettesítenek.) Az axiomaOK?(??) szabályoktól származnak, és azt jelzik, hogy az érintett ?-axióma rendben találtatott a legfeljebb ?? hosszúságú sorozat esetén. Ami csak sejthető: az „S: […] (??)” kiírások értelme. Lássuk a magyarázatot!
Ahhoz, hogy a program belássa valamely axióma helyességét egy nem 0 hosszúságú sorozatra, szükség van egy ilyen hosszúságúra. Tehát a program engedve a bizonyit? szabálybeli „N+1=N? and axiomaOK?(N?)” felhívásnak, létre hozatja (az axiomaOK? szabályban szereplő hossz(V,N1) segítségével) a kívánt (ottani jelölés szerint: N1) hosszúságú sorozatot.
Figyelmünket szenteljük a hossz szabályra! A kérdéses (N1) hosszúságú sorozat előállítása rekurzívan történik. Előbb az N1-1 hosszúságút, majd … az 1, s végül a 0 hosszúságút, ami egyetlen van: mégpedig az [] („hossz([],0).”). Itt ér véget a rekurzió. S a „hossz([_|S],H) if hossz(S,HH) and H=HH+1.” szabálynak megfelelően már építhető az 1 ([_]), majd … az N1-1, s végül az N1 hosszúságú sorozat. Az utóbbit már maga az „axioma?(verem([N|V],def),igaz)” hívás teszi hozzá.
Az elmondottak könnyebb megértése kedvéért a hivatkozott szabálykötegeket egybenyaláboltuk:
|
bizonyit4(N) if |
A bizonyit4 szabály azon részlete, amely a 4º axióma
helyességét firtatja: []-re
igaz-e; ha igen, |
|
axiomaOK4(N) if |
4º axióma akkor igaz legalább N eleműre, ha és az axióma teljesül olyan N+1 eleműre is, amelyek első elemének értéke pontosan N. |
|
hossz([],0). |
0-hosszúságú sorozat csak a []. |
Megjegyzés: Nem használjuk ki a továbbiakban a JegyezdfelA szabály funkcióját, nyugodtan elhagyható. Nem korlátozza a bizonyítás erejét az a tény, hogy „csak” N kezdetű sorozatokra látjuk be a helyességét, mivel a sorozat elemeinek milyensége nem, csak a sorrendje fontos. Az „aktív” végén levő elem többitől megkülönböztethetősége fontos az egyes axiómákban, ezért nem írhattuk így:„…axioma4(verem([_|V],def),igaz)…”.
… és a kiírás hogyan került ki? Nos az 1º axiómának van egy különlegessége. Hivatkozik feltételek tagadására is. Az ilyen szabályokat a Prolog csak úgy képes megoldani –paraméterek esetleges előállítási „kényszere” esetén, ami most fennáll–, ha van mire építeni a tagadásban szereplő paramétereket. Egyszerűen szólva: csak „pozitív” kijelentéssel kezdődhet egy ilyen szabály. Nos ezt a biztos alapot szolgáltatja a sorozatok szabály, amely nagyon hasonlít a hossz-ra, sőt működése lényegileg azonos is. Ezt a szabályt egészítettük ki egy kiírással (a jegyezdfelS szabályban), amely a programunk működésének kulisszatitkaiba való bepillantást tette lehetővé. Valójában nem tartozik a működés lényegéhez a jegyezdfelS szabály, ezért minden további nélkül elhagyható[3].
|
axioma1(verem(V,def),igaz) if |
A sorozatok generál egy megfelelő elemszámú V
sorozatot. |
|
sorozatok([]).
|
Kiindulásul az üres sorozat áll rendelkezésre… … és az egy elemmel bővítés szabálya, amely a hosszal szinkronban generálja az új elemet, majd feljegyzi azt. A sorozatok(S) utáni rész elhagyható, ha a „nyomkövetés” szükségtelen. |
Az adminisztrációnál, mivel az axiómákat eddig sorszámukkal jegyeztük föl, negatív sorszámmal azonosítjuk a „hiba-axiómákat”. Pl.:
|
axiomaOK4H(N) if |
… ha a 4’º hiba-axióma kielégíthetőnek bizonyult, akkor jegyezzük föl … |
A teljes programot tekinthetjük meg az A. függelékben.
Irodalom
Kozma L. – Varga L.: „Adattípusok osztálya.”, ELTE TTK Informatikai TanszékCsoport, 2001
Szlávi P.: „Programok, programspecifikációk.”, Informatika a felsőoktatásban’99 konferencia, Debrecen, 1999
Programhivatkozások
Szlávi P.: „A sor specifikációinak kompatibilitását ellenőrző
Prolog program.”,. http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/SOR1.PRO
Szlávi P.: „A sor specifikációinak kompatibilitását ellenőrző
Prolog program – hibás az Első operáció specifikációja.”,. http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/SOR1H1.PRO
Szlávi P.: „A sor specifikációinak kompatibilitását ellenőrző
Prolog program – hibás a Sorba operáció specifikációja.”,. http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/SOR1H2.PRO
Szlávi P.: „A sor specifikációinak kompatibilitását ellenőrző
Prolog program – hibás a Sorba operáció error-specifikációja.”,. http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/SOR1H3.PRO
Szlávi P.: „A sor specifikációinak kompatibilitását ellenőrző
Prolog program – FIFO-ság ellenőrzése.”,.
http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/SORALL.PRO
Szlávi P.: „A verem specifikációinak kompatibilitását
ellenőrző Prolog program – strukturális indukció alapján.”,. http://izzo.inf.elte.hu/szlavi/Doktori/TipSpecKomp/VERSTIN3.PRO
Függelék
A. Verem specifikációinak összevetését végző Prolog program listája.
Azokat a részeket mellőztük, amelyek könnyen származtathatók az „előzményeiből”.
Domains
TNemDef = nemDef; def
TElem = Integer
TSorozat = TElem*
TVeremK = verem(TSorozat,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 */)
/* hiba-axióma: */
axioma3H(TVeremK,TLogikai /*
teljesül-e */)
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 */)
/* hiba-axióma: */
axioma4H(TVeremK,TLogikai /*
teljesül-e */)
axioma4H_1(TVeremK,TLogikai /*
teljesül-e */)
hossz(TSorozat,Integer)
sorozatok(TSorozat)
jegyezdfelS(TSorozat,Integer)
axiomaOK1(Integer)
axiomaOK1_1(Integer)
…
axiomaOK4H(Integer)
axiomaOK4H_1(Integer)
jegyezdfelA(Integer /*axióma
sorszám*/, Integer /*sorozathossz*/).
bizonyit1(Integer)
…
bizonyit4H(Integer)
Database – axiomak
keszAxiomaOK(Integer
/*axióma sorszám*/, Integer /*sorozathossz*/)
Clauses
%
alap rutinok:
hossz([],0).
hossz([_|S],H) if
hossz(S,HH) and H=HH+1.
sorozatok([]).
sorozatok([E|S]) if
sorozatok(S) and
hossz(S,N) and N+1=NN and
hossz([E|S],NN) and
jegyezdfelS([E|S],NN) /*ez
elhagyható*/.
jegyezdfelS(S,N) if
Write(„S: „,S,” („,N,”)”) and
nl.
%
algebrai és P/P-specifikáció:
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(verem(V,def),igaz) if
axioma1_2(verem(V,def),igaz).
axioma1(_,hamis).
axioma1_1(V,igaz) if
ures(V) and uresE(V,igaz).
axioma1_2(verem(V,def),igaz) if
sorozatok(V) and
not(ures(verem(V,def))) and
not(uresE(verem(V,def),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(V,def),igaz) if
axioma3H_1(verem(V,def),igaz).
axioma3H(_,hamis).
axioma3H_1(verem(V,def),igaz) if
uresE(verem(V,def),igaz) and
! and
teto(verem(V,def),_,verem(_,nemDef))
or
uresE(verem(V,def),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).
%
kompatibilitás ellenőrzés:
axiomaOK1(X) if
keszAxiomaOK(1,X).
axiomaOK1(0) if
axioma1(verem([],def),igaz) and
jegyezdfelA(1,0).
axiomaOK1(N) if
axiomaOK1_1(N).
axiomaOK1(N) if
write(„Az 1. axióma specifikációi
nem kompatibilisek. („,N,”)”) and
nl and fail.
axiomaOK1_1(N) if
N-1=N1 and N1>=0 and
axiomaOK1(N1) and
hossz(V,N1) and
axioma1(verem([N|V],def),igaz) and
jegyezdfelA(1,N).
…
axiomaOK4H(X) if
keszAxiomaOK(-4,X).
axiomaOK4H(0) if
axioma4H(verem([],def),igaz) and
jegyezdfelA(-4,0).
axiomaOK4H(N) if
axiomaOK4H_1(N).
axiomaOK4H(N) if
write(„A 4H. axióma specifikációi
nem kompatibilisek. („,N,”)”) and
nl and fail.
axiomaOK4H_1(N) if
N-1=N1 and N1>=0 and
axiomaOK4H(N1) and
hossz(V,N1) and
! /*visszalépéskor az axióma
sérül*/ and
axioma4H(verem([N|V],def),igaz) and
jegyezdfelA(-4,N).
jegyezdfelA(Ax,N) if
keszAxiomaOK(Ax,N)
or
Assert(keszAxiomaOK(Ax,N),axiomak) and
Write(„AxOK”,Ax,”(„,N,”)”) and
nl and
save(„axioma.dba”,axiomak).
bizonyit1(N) if
not(axiomaOK1(0)) /*már a
0-eleműre sem OK*/
or
% axiomaOK1(0) /*0-eleműre OK*/ and
jegyezdfelA(1,N) /*indukciós
feltétel*/ and
N+1=N1 and axiomaOK1(N1)
/*következtetés N-ről N+1-re*/.
…
bizonyit4H(N) if
not(axiomaOK4H(0)) /*már a
0-eleműre sem OK*/
or
% axiomaOK4H(0) /*0-eleműre
OK*/ and
jegyezdfelA(-4,N) /*indukciós
feltétel*/ and
N+1=N4H and axiomaOK4H(N4H)
/*következtetés N-ről N+1-re*/.
Goal
%
inicializálás:
clearwindow
and
% a
komaptibilitás ellenörzése strukturális indukcióval:
N=5
/*inputparaméter, nem ellenörzöm*/ and
%
strukturális indukció,
% nem épít arra, hogy kisebb N-ekre már belátta:
% 1.
axióma:
bizonyit1(N)
and ! /*a visszalépés
értelmetlen*/ and
…
% 4H.
axióma:
bizonyit4H(N)