21.4.Az absztrakt program tulajdonságai

21.4.Az absztrakt program tulajdonságai
Előző	21. fejezet - Párhuzamos absztrakt program	Következő

Az absztrakt programok tulajdonságait az állapottér hatványhalmaza felett értelmezett relációkkal írjuk le. A könyv első részében már ismertetett leggyengébb előfeltétel fogalmát általánosítjuk és ennek segítségével határozzuk meg a programtulajdonságokat. Leggyengébb előfeltételt a program szövege alapján tudunk számolni, a tulajdonságok tehát statikusan, a program működésének vizsgálata nélkül meghatározhatóak.

21.4.1.A leggyengébb előfeltétel és általánosítása

Az absztrakt programok jellemzésekor támaszkodunk a leggyengébb előfeltétel [[???Dij 76, ???Fót 83]], a legszigorúbb utófeltétel [[???Lam 90]], ill. a monoton leképezések fixpontjának (. fejezet) fogalmára.

21.25. Definíció (Leggyengébb előfeltétel, legszigorúbb utófeltétel).
Legyen egy utasítás, pedig logikai függvények az állapottér felett. A logikai függvény az utófeltétel utasításra vonatkozó leggyengébb előfeltétele, ahol . Az logikai függvény a előfeltétel legszigorúbb utófeltétele az -re nézve, ahol .

21.6. Lemma.
(Leggyengébb előfeltétel alaptulajdonságai)
(csoda kizárásának elve),
Ha , akkor ,
(utófeltételbe helyettesítés módszere),
Ha , akkor (monotonitás),
(gyenge additivitás),
(multiplikativitás).

Biz.: Az állítások közvetlenül a . definícióból következnek. ((1), (3), (4), (5), (6) bizonyítása megtalálható [[???Fót 83, ???Fót Hor 91]]-ben.)

21.8. Megjegyzés.
A lemma (2)-es állítása az absztrakt programban előforduló utasításokra, a feltételes értékadásokra (. def.) mindig teljesül.

21.7. Lemma.
(Kiterjesztés és leggyengébb előfeltétel) Legyen az altéren definiált logikai függvény, pedig az logikai függvény kiterjesztése -ra. jelölje az utasítás -ra vonatkozó kiterjesztését. Legyen egy tetszőleges olyan pont, amelyre , Ekkor: és

Biz.: és (a . lemma alkalmazásával) és . A legszigorúbb utófeltételre vonatkozó állítás ugyanígy bizonyítható.

21.1. Következmény.
és .

21.8. Lemma.
(Kiegészítés és leggyengébb előfeltétel) Ha , akkor és . Ha , akkor .

Biz.: Ha , akkor (. lemma). Ha , akkor .

21.9. Lemma (Szuperpozíció és leggyengébb előfeltétel).
Legyen egy-egy logikai függvény és , . Ekkor , ill. ha , akkor .

Biz.: A . lemmát többször alkalmazva bizonyítunk. A feltétel szerint , azaz . A feltétel szerint és , így , azaz . A . lemma szerint , így éppen a lemma állítását kaptuk.

A továbbiakban jelöljön egy absztrakt programot (. def.), az állapottér legyen . , ahol és egy (szimultán, nemdeterminisztikus) feltételes értékadás. .

Általánosítjuk a leggyengébb előfeltétel fogalmát:

21.26. Definíció (Leggyengébb előfeltétel általánosítása).
. ( az ún. ”angyali” leggyengébb előfeltétel [[???Mor 90]]). A leképezés definíciója hasonlít a J.R. Rao által egyes utasításokra definiált operátor definíciójához, de attól eltérően absztrakt programra vonatkozik. A operátort a UNITY valószínűségi alapon nemdeterminisztikus kiegészítése során használják [[???Rao 95]].

21.10. Lemma.
(Általánosított leggyengébb előfeltétel alaptulajdonságai)
,
,
Ha , akkor ,
,
.

Biz.: Az állítások az a . definícióból, a . lemmából és a logikai és függvénykompozíció asszociativitásából és kommutativitásából következnek.

21.4.2.Invariánsok és elérhető állapotok

Jelöljük -val azon logikai függvények igazsághalmazainak halmazát, amelyek az programra nézve invariánsokSzigorú invariáns [[???Pra 94]]., ha a program -beli állapotból indul. A -t röviden -val jelöljük. Jelölje azon logikai függvények konjunkcióját, amelyekre a legszigorúbb invariáns [[???Pra 94]]..

21.27. Definíció (Invariáns tulajdonság).
. . .

21.2. ábra -

21.2. ábra. Invariáns ( ) és mindig igaz ( ) tulajdonság.

21.9. Megjegyzés ( nem üres).
A definíció szerint .

21.11. Lemma.
(Invariánsok konjunkciója) zárt a műveletre nézve [[???Pra 94]].

Biz.: Legyen . . def. felhasználásával: és . és . A . lemma szerint: , így .

21.2. Következmény (Legszigorúbb invariáns).
Az halmaznak egyértelműen létezik legkisebb (. def.) eleme és az éppen .

21.28. Definíció (Legszigorúbb invariáns).
Az halmaz legkisebb elemét, -t a legszigorúbb invariánsnak nevezzük.

21.12. Tétel.
(Invariáns konjunkciója kezdetben igaz állítással) Ha , és , akkor ( invariáns).

Biz.: Ha , akkor . Így az első feltétel szerint. Ha , akkor , a harmadik feltétel és . lemma felhasználásával: .

21.10. Megjegyzés (Invariáns tulajdonság felbontása).
A . tétel nem megfordítható. Ha invariáns, akkor nem feltétlenül igaz, hogy akár , akár invariáns lenne. Annak bizonyítása, hogy egy állítás invariáns tulajdonság, a . tétel segítségével azonban sok esetben részekre bontható pl. úgy, hogy
belátjuk, hogy invariáns,
megmutatjuk, hogy kezdetben igaz,
igazoljuk, hogy , ahol .

21.29. Definíció (Mindig igaz).
. . .

21.11. Megjegyzés ( nem üres).
A definíció szerint .

Azokat a logikai függvényeket, amelyek igazsághalmaza eleme a halmaznak, a -ból elérhető állapotok felett a program futása során mindig igaz állításoknak nevezzükA mindig igaz állításokat gyenge invariánsoknak is nevezik [[???San 91, ???Pra 94]].

A . ábra segítségével szemléltetjük, hogy van olyan mindig igaz állítás, amelyik nem invariáns. Tegyük fel, hogy a körrel jelölt mezőből indul egy huszár, amely lólépésben haladhat. Az állapottér az összes mező, a hiányos ”sakktábláról" lelépni nem szabad. Könnyen ellenőrizhetjük, hogy a huszár mindig ”x”-szel jelölt mezőkön marad. Mégsem invariáns tulajdonsága a huszárnak az, hogy ”x”-szel jelölt mezőn áll, mert van olyan ”x”-szel jelölt mező amelyről jelöletlen mezőre is léphet. Ilyen a bal felső sarokban lévő mező. Ez a mező a huszár számára nem elérhető, ezért sohasem tapasztaljuk az invariáns sérülését. Megállapíthatjuk, hogy a mindig igaz és az invariáns állítások között a lényegi különbség a nem elérehető állapotok esetén jelentkezik. Egy invariáns állítás még nem elérhető állapotokból is megmarad, egy mindig igaz állítás csak az elérhető állapotok felett teljesül. Az invariáns állítások azért fontosak, mert két komponens együttműködése könnyen eredményezheti azt, hogy korábban el nem érhető állapotok elérhetővé válnak. Több komponensből álló elosztott programok esetén tehát csak az invariáns tulajdonságokra támaszkodhatunk (ld. fejezet).

21.3. ábra -

21.3. ábra. Egy mindig igaz állítás nem mindig invariáns.

21.13. Lemma.
(Az invariáns mindig igaz) . Biz.: A . következmény szerint, ha .

21.14. Lemma.
(Mindig igaz állítások konjunkciója mindig igaz) Ha és , akkor .

Biz.: Ha , akkor és . Így . Ha , akkor és . Így .

21.3. Következmény.
Mindig igaz és invariáns konjunkciója mindig igaz.

21.4. Következmény (A legszigorúbb mindig igaz).
A halmaznak egyértelműen létezik legkisebb eleme és az éppen , a legszigorúbb invariáns.

tehát az a legszűkebb igazsághalmazú logikai függvény, amelyiknek igazsághalmazát a program soha nem hagyja el a -ból indulva. Így kimondhatjuk az alábbi tételt:

21.15. Tétel.
( és a -ból elérhető állapotok) igazsághalmaza éppen a -ból elérhető állapotok (. def.) halmaza [[???Pra 94]].

Nem minden esetben lesz egy mindig igaz állítás és egy invariáns konjunkciója invariáns, hiszen pl. az is invariáns és konjunkciója egy mindig igaz, de nem invariáns állítással nem eredményezhet invariáns állítást.

21.16. Lemma.
(Mindig igaz és invariáns konjunkciója) Ha , és , akkor . Biz.: Ha , akkor . Így az állítás következik a . tételből.

21.4.3.Biztonságossági tulajdonságok

Jelöljük -sel azon logikai függvények igazsághalmazai rendezett párjainak halmazát, amelyekre az program végrehajtása során igaz, hogy stabil feltéve, hogy nem . Jelölés: .

21.30. Definíció (Stabil feltéve, hogy – tulajdonság).
. A definíciója megfelel a [[???Cha Mis 89]]-ben adott unless fogalmának.

21.12. Megjegyzés (Stabil tulajdonság).
Azt mondjuk, hogy rendelkezik a stabil tulajdonsággal, ha .

21.17. Lemma.
( és a stabil tulajdonságok) Ha és , akkor . Biz.: A . def. alapján és . Ebből a . lemma alkalmazásával: = = . A . def. alkalmazásával a kívánt állításhoz jutunk.

21.18. Lemma.
(Az invariánsok stabil tulajdonságok) Ha , akkor . Biz.: A . és . definíciók közvetlen következménye.

21.19. Tétel.
( és az invariánsok szigoríthatósága) Ha és és , akkor és A tétel Prasetya tételének relációs átfogalmazása [[???Pra 94]].. Biz.: Az állítás első része következik a . lemmából. Az állítás második részét pedig a . és . lemma alkalmazásával kapjuk.

21.20. Tétel.
( és a legszigorúbb invariáns) Ha és , akkor . Biz.: miatt alkalmazható a . tétel. def. alapján viszont .

21.4. ábra -

21.4. ábra. tulajdonság és invariáns kapcsolata.

21.4.4.Haladási tulajdonságok

Jelöljük -sel azon logikai függvények igazsághalmazai rendezett párjainak halmazát, amelyekre az program végrehajtása során igaz, hogy stabil feltéve, hogy nem és van egy olyan feltételes értékadás, amely garantálja, hogy a -ből -ba jutunk. Jelölés: .

21.31. Definíció (Biztosítja tulajdonság).
. A definíciója megfelel a [[???Cha Mis 89]]-ben adott ensures fogalmának, ha az ütemezés megfelel a feltétlenül pártatlan ütemezés axiómájának.

21.21. Lemma.
( és a stabil tulajdonság) Ha és , akkor .

Biz.: A . def. és a . lemma alapján elegendő azt bizonyítani, hogy . A feltételekből tudjuk, hogy . Válasszunk egy ilyen utasítást. stabil, ezért erre az -re is: . Az -re vonatkozó két állításból logikai és művelet és egyszerűsítés után a eredményre jutunk. A leggyengébb előfeltétel ismert tulajdonsága alapján (. lemma) .

21.22. Tétel.
( és az invariánsok szigoríthatósága) Ha és és , akkor és A tétel Prasetya tételének relációs átfogalmazása [[???Pra 94]].. Biz.: Az állítás első része következik a . lemmából. Az állítás második részét pedig a . és . lemma alkalmazásával kapjuk.

21.23. Tétel.
( és a legszigorúbb invariáns) Ha és , akkor . Biz.: . tételhez hasonlóan.

21.32. Definíció (Elkerülhetetlen tulajdonság).
Legyen a reláció tranzitív diszjunktív lezártja (. def.), vagyis az a legkisebb relációA definíciója megfelel a [[???Cha Mis 89]]-ben adott leads-to fogalmának, ha az ütemezés megfelel a feltétlenül pártatlan ütemezés axiómájának., amelyre teljesül, hogy

.
Tranzitivitás: ha és , akkor .
Diszjunkció: ha bármely W megszámlálható halmazra: .

Jelölés: .

A . def. alapján pontosan akkor, ha a . def. (1),(2),(3) szabályainak alkalmazásával levezethetőA (3)-as szabály egyetlen lépésben is végtelen sok elemre alkalmazható..

21.13. Megjegyzés (Egyértelműen létezik legkisebb adott tulajdonságú reláció).
A rendelkezik a megadott tulajdonságokkal. Ha és rendelkezik a megadott tulajdonságokkal, akkor is rendelkezik velük. Így egyértelműen definiált.

21.14. Megjegyzés.
A UNITY különböző relációs kiterjesztéseiben [[???Pac 92, ???Jut Kna Rao 89]] nem a feladat specifikációs feltételeinek, hanem a program által definiált , , relációknak megfelelő relációkat definiálnak. Pachl [[???Pac 92]] az reláció értelmezési tartományát az elérhető állapotok halmazára (. def.) korlátozza.

21.24. Lemma.
( és ) Ha , akkor tetszőleges programra. Biz.: , így a . definíció szerint.

21.25. Lemma.
( és a stabil tulajdonság) Ha és , akkor .

Biz.: Strukturális indukcióval az induktív . def. alapján. Alapeset: -t közvetlenül -ból kaptuk. Ekkor a . lemma szerint . . def. (1) pontja szerint ekkor . Indukciós feltevés: a) eset: az utolsó lépésben a . def. (2) pontját, a tranzitivitást alkalmaztuk előállításakor, azaz: és . Az indukciós feltétel szerint: és . A . def. (tranzitivitás) alapján: . b) eset: az utolsó lépésben a . def. (3) pontját, a diszjunktivitást alkalmaztuk előállításakor, azaz: és . Az indukciós feltétel szerint: , amiből a . def. (diszjunktivitás alapján) .

21.15. Megjegyzés.
A tétel általánosítható a következő alakbanA PSP tétel [[???Cha Mis 89]] relációs alakja.: Ha és , akkor . Bizonyítás strukturális indukcióval.

21.26. Tétel.
( és az invariánsok szigoríthatósága) Ha és és , akkor és A tétel Prasetya bizonyítás nélkül publikált tételének relációs átfogalmazása [[???Pra 94]]. .

Biz.: Az állítás első része következik a . lemmából. Az állítás második részét pedig a . és . lemma alkalmazásával kapjuk.

21.27. Tétel.
( és a legszigorúbb invariáns) Ha és , akkor . Biz.: . tételhez hasonlóan.

21.28. Tétel.
( egyelemű részhalmazokra) . Biz.: Ha , akkor . def. alapján (diszjunktív lezárás). Ha , akkor . A . lemma alapján . Ha , akkor a tranzitív lezárás miatt .

21.29. Lemma.
( – jobboldal gyengítése) Ha és , akkor . Biz.: . lemma és a . def. (tranzitivitás) következménye.

21.33. Definíció (Elkerülhetetlen feltétlenül pártatlan ütemezés mellett).
, akkor és csak akkor, ha az által az -hoz rendelt fákban bármelyik, a feltétlenül pártatlan ütemezésnek megfelelő végrehajtási útonv.ö. . def. véges (esetleg nem korlátos) távolságban van olyan pont, amelynek címkéje eleme halmaznak.

21.30. Tétel.
( egyelemű részhalmazokra) . Biz.: A . def. közvetlen következménye.

21.31. Tétel.
( helyessége és teljessége) = A tétel Pachl tételének általánosítása [[???Pac 92]].
Biz.:[[???Pac 92]]-ben adott bizonyítás általánosítható a teljes állapottérre (lásd lábjegyzet) és nemdeterminisztikus feltételes értékadások esetére. a) . Biz.: és tranzitív és diszjunktív. b) . A ., . tételek alapján elegendő bizonyítani, hogy . . . Legyen . Jelöljük -vel azon pontok halmazát, amelyekre igaz, hogy -ből olyan úton érhetőek el, amelynek minden pontja eleme -nek. , ellenkező esetben , azaz és miatt következne, ami ellentmondás. Tehát -re megkonstruálható egy olyan út, amelyen címkéje szerepel a feltétlenül pártatlan ütemezés axiómája szerint és az út belsejében halad. Tegyük fel indirekt, hogy . Ekkor a fentiek alapján . Azaz , azaz .

21.5. Következmény.
Ha egy program rendelkezik a tulajdonsággal, akkor és csak akkor rendelkezik a tulajdonsággal is, amely a tranzitivitás és a diszjunkció szabályának alkalmazásával levezethető a program alakú tulajdonságaiból A tranzitív diszjunktív lezárási tulajdonságok felhasználásával Cook-féle relatív teljes [[???Rao 95]] levezetési szabályrendszert alkothatunk a program haladási tulajdonságaira nézve..

21.4.5.Fixpont tulajdonságok

A konkrét program az absztrakt program végrehajtásának prefixe. Az absztrakt program nem terminál abban az értelemben, hogy több elemi művelet nem kerül végrehajtásra. Termináltnak tekinthetünk azonban egy izolált programot akkor, ha elérte egy fixpontját, azaz a további műveletek hatására állapotváltozás már nem következhet be.

Az programról azt mondjuk, hogy fixpontba jutott az altér felett, ha az altérhez tartozó változókra vonatkozó egyszerű értékadások mindegyikére teljesül, hogy az értékadás hatásrelációja független az altérhez nem tartozó állapottérkomponensektől és

az értékadás determinisztikus és a jobboldalán álló függvénykompozíciók (kifejezések) értéke azonos a baloldalon álló változók értékével vagy
az értékadás jobboldalán szereplő kapcsoszárójel függvény feltétele hamis, vagy
az értékadás nemdeterminisztikus és az altér azon részhalmazának, amely felett az értékadás determinisztikus, és a kapcsoszárójel függvény feltétele igazsághalmazának metszete felett az értékadás jobboldalán álló függvénykompozíciók (kifejezések) értéke azonos a baloldalon álló változók értékével.

Legyen , ahol egy (szimultán, nemdeterminisztikus) feltételes értékadás, .

Jelöljük -vel azt a logikai függvényt, amelynek igazsághalmazára leszűkítve az reláció determinisztikus, azaz: .

21.34. Definíció (Fixpontok halmaza).

Ha az értékadások mindegyike determinisztikus, akkor a program fixpontjait jellemző logikai függvényt a szimultán értékadások egyenlőséggé való átalakításával, feltételeik implikációs előtaggá való kiemelésével és konjunkciójával kapjuk meg: .

21.2. Példa (Program fixpontjainak halmaza).
. [[???Cha Mis 89]].

21.35. Definíció (Fixpont tulajdonság).
Jelöljük -sel azon logikai függvények igazsághalmazainak halmazát, amelyekre .

21.16. Megjegyzés.
A megoldás definíciója szerint (.) egy program teljesíti a specifikációs feltételt, ha az fixpontfeltétel tartalmazza a állítás igazsághalmazának és (legalább) az elérhető állapotok halmazának metszetét.

21.32. Lemma.
(Fixpont tulajdonság gyengítése) Ha és , akkor . Biz.: Az . def. közvetlen következménye.

21.4.6.Terminálási tulajdonságok

21.36. Definíció (Biztosan fixpontba jut – tulajdonság).
Jelöljük -sel azon logikai függvények igazsághalmazainak halmazát, amelyekre .

A program biztosan fixpontba jut, ha egy alkalmasan megválasztott variáns függvény pl. az állapottér változóiból függvénykompozícióval alkotott nemnegatív egészértékű függvény értéke bármely állapot elérése után a jövőben elkerülhetetlenül csökken (. tétel).

Előző	Fel	Következő
21.3.Pártatlan ütemezés fogalma	Tartalom	21.5.Az absztrakt program viselkedési relációja