24. fejezet - Programkonstrukciók
Előző III. rész - Párhuzamos és elosztott programozás (Horváth Zoltán) Következő

24. fejezet - Programkonstrukciók

Tartalom

24.1.Unió
24.2.Szuperpozíció
24.3.Szekvencia

Ebben a fejezetben programok és feladatok konstrukciós módszereit ismertetjük, azaz megadjuk, hogy meglévő feladatokat hogyan bonthatunk részfeladatokra, illetve programokból milyen szabályok alapján hozhatunk létre összetett programot. Bevezetjük a kompozícionális modell fogalmát, majd megvizsgáljuk, hogy a programkonstrukciós szabályokkal kiegészített modell mennyiben felel meg a kompozícionalitás követelményének.

Feladatok és programok konstrukcióit, mint egy vagy több relációhoz egy relációt hozzárendelő leképezéseket definiáljuk.

Megengedett konstrukciós műveletnek nevezünk a továbbiakban minden olyan relációs műveletet, amely - relációk uniója, metszete, különbsége, - relációk adott pontban felvett értékének uniója, metszete, különbsége, - relációk vetítése, kiterjesztései, rendezett reláció -esek komponenseire bontása és komponensekből rendezett reláció -esek előállítása, - relációk direkt szorzata, - relációk kompozíciója, szigorú kompozíciója és lezártjai (lezárt, korlátos lezárt, tranzitív, diszjunktív lezárt), véges sokszori egymás utáni alkalmazásakéntA definíció nem formális. A modell keretein túlmutat annak vizsgálata, hogy a fent felsorolt elemi műveletek valamilyen értelemben teljes rendszert alkotnak-e. megfogalmazható.

A modellben feladatkonstrukciónak nevezzük azokat a megengedett konstrukciós műveleteket, amelyek egy vagy több feladatból egy feladatot állítanak elő. Programkonstrukciónak nevezzük azokat a megengedett konstrukciós műveleteket, amelyek egy vagy több programból egy új, összetett programot állítanak elő.

24.1. Definíció.

Kompozícionálisnak nevezünk egy programozási modellt, ha a modell minden feladatkonstrukciójához létezik olyan programkonstrukció, hogy megoldása és megoldása esetén megoldja -t.

24.2. Definíció.

Részlegesen kompozícionális egy programozási modell, ha egyes kiválasztott feladatkonstrukciók esetén megadható olyan programkonstrukció, amelyre megoldása és megoldása esetén megoldja -t.

A továbbiakban megmutatjuk, hogy a bevezetett modell részlegesen kompozícionális.

Jelöljük az program viselkedési relációját -vel, az program viselkedési relációját -vel.

24.1.Unió

24.3. Definíció (Unió).

Legyen az tér az állapottér altere. Jelölje az terek legnagyobb közös alterét. Legyen az , az altér felett definiált program kiterjesztése (. def.) -ra. , . Az programot, amely az állapottéren adott, az és program uniójának nevezzük és -vel jelöljük, ha minden altérhez tartozó változóra teljesül, hogy az és értékadások azonos értéket rendelnek hozzá, azaz: és , ,

24.1. Tétel.

(Unió viselkedési relációja) Legyen . EkkorA tétel (1)-es,(2)-es és (5)-ös pontja a UNITY unió tételének relációs alakja [[???Cha Mis 89]].:

  • -ra, amelyre : Az állítás általánosítható: ha and , akkor .

  • .

Biz.:

(1) A . és a . def. alapján: .

Tegyük fel, hogy . Ekkor a . def. és a egyenlőség felhasználásával: . A jobboldal gyengítésével: ill. , azaz és . Ha és , akkor és , így . A bizonyított egyenlőség és a . def. alapján: .

(2) Tegyük fel, hogy . A . def. szerint { (1) és a . def. felhasználásával } , és , azaz { . def. } és és ( vagy ).

(3) A . def. és (2) következménye.

(4) Tegyük fel, hogy és . A . def. szerint ekkor és . Ekkor is teljesül, így a feltétel miatt . A . def. alapján és . A . és . def. szerint .

(5) . def. és . def. közvetlen következménye.

(6) (5) következménye. Ha és , akkor .

(7) A . def. és a (3),(5) állítások következménye.

24.1. Megjegyzés ( ).

A . tétel (3) pontjának bizonyításához felhasználtuk, hogy és esetén is teljesül. Ez a segédállítás nem megfordítható. A . példa segítségével megmutatjuk, hogy az összetett program invariánsa nem invariánsa az összetevőknek.

24.1. Példa.

. . . . Könnyen ellenőrizhető, hogy , . , de ill. .

24.2. Megjegyzés ( ).

Az előző megjegyzésben leírt gondolatmenethez hasonlóan belátható, hogy és .

24.3. Megjegyzés ( és ).

A logikai függvény, ill. a reláció meghatározható az összetevő programok viselkedési relációjából, így . és a . def. alapján a ill. a reláció is kifejezhető közvetett módon az összetevő komponensek viselkedési relációjából a tétel (3) és (7) pontja szerint. Az unió viselkedési relációjának egyes komponensei, pl. , ill. általában azonban nem határozhatóak meg az összetevő programok viselkedési relációjának megfelelő komponenseiből. Az alábbi példa (.) szerint általában nem igaz, hogy és esetén is teljesül.

24.2. Példa ( ).

. . . . A . def. alapján könnyen igazolható, hogy és . A . tétel alapján, ha van olyan feltétlenül pártatlan ütemezésnek megfelelő végrehajtási útja -nek, amely mentén -ből elkerülhető , akkor nem teljesül. Válasszuk kezdőállapotnak az állapotot. Az ütemezés feltétlenül pártatlan és sohasem jut a program -beli állapotba.

Jelöljük -fel az feladatot megoldó programok halmazát.

24.4. Definíció (Feladatok egyesítése).

Legyen és közös állapot és paramétertérenHa az állapottér nem közös, akkor válasszunk egy olyan teret, amelynek mindkét állapottér altere. A feladatokat terjesszük ki a közös térre (. def.). adott feladat. { ( , , ) }.

24.2. Tétel.

(Unió levezetési szabálya) Legyen és az állapottér és a paramétertér felett megadott feladat. és az állapottérre kiterjesztett programok, amelyek uniója értelmezett (. def.). Ha megoldja -et mellett és megoldja -t mellett és , akkor megoldja -t.

Biz.: ., . def. és . tétel következménye.

Az unió levezetési szabálya (. tétel) azt mondja ki, ha a modell szemantikája összefésüléses és az összetevők rendelkeznek egy közös globális invariánssal [[???And 91]], akkor az ezen invariáns tulajdonság mellett megoldott feladatok megfelelő kompozícióját az összetett program is megoldja. A . példán megmutatjuk, hogy az összefésüléses szemantika milyen lényeges az unió viselkedési relációjának meghatározhatóságában [[???Cha 90]].

Bizonyos esetekben programok uniójának viselkedési relációja könnyen kifejezhető az összetevők viselkedési relációja alapján. Ez akkor lehetséges, ha az összetevők kölcsönhatása (interferenciája) az unió levezetési szabályában tett megszorításokon túl további tulajdonságokkal is jellemezhető.

A kölcsönhatás jellemzésének alkalmas módja lehet a nyitott specifikáció, amely az eredő program egyszerűbb (általában biztonságossági) tulajdonságaira tett kikötések segítségével tesz indirekt kikötéseket az egyik vagy mindkét összetevő tulajdonságaira. A nyitott specifikáció módszerét részletesen bemutatja Chandy és Misra [[???Cha Mis 89]].

A szekvencia programkonstrukció esetében (. def.) az unió olyan speciális esetét fogalmazzuk majd meg, ahol a unióhoz tartozó értékadásokat olyan diszjunkt csoportokba sorolhatjuk, hogy az állapottér egy alkalmasan megválasztott részhalmaza felett legfeljebb egyetlen csoporthoz tartozó értékadások hatásrelációi különböznek az identitástól. Az alábbi két tétel erre a speciális esetre vonatkozik.

24.3. Tétel.

(Unió és az állapottér részhalmazai) Legyen , logikai függvény az állapottéren oly módon, hogy és . Ekkor

  • ha , akkor ,

  • ha , akkor ,

  • ha , akkor .

Biz.: A feltétel alapján: , így: . (1) A feltételek és . lemma szerint: és .

(2) Az előző állítás szerint: . A feltétel és . lemma szerint: . Ha , akkor , így az állítást igazoltuk.

(3) Strukturális indukcióval az induktív . def. alapján. Alapeset: -t 1 lépésben vezettük le -ból. Az előző állítás szerint ekkor , az . def. szerint: . Indukciós lépés: a) eset: az utolsó lépésben a . def. (2) pontját, a tranzitivitást alkalmaztuk, 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, azaz: és . Az indukciós feltétel szerint: , amiből a . def. (diszjunktivitás alapján) .

A tétel egy kicsit módosított feltételekkel is kimondható. A (3)-as állítás megfogalmazásánál alkalmazzuk a nyitott specifikáció módszerét.

24.4. Tétel.

(Unió és az állpottér részhalmazai (2.)) Legyen , logikai függvény az állapottéren oly módon, hogy , . Ekkor

  • ha , akkor ,

  • ha , akkor ,

  • ha és , akkor .

Biz.: A feltétel alapján: , így: . (1) A feltételek szerint: és . A . lemma alapján: és .

(2) Az előző állítás szerint: . A feltétel szerint: . . Ha , akkor , így az állítást igazoltuk.

(3) Struktúrális indukcióval az induktív . def. alapján. Alapeset: -t 1 lépésben vezettük le -ból. Az előző állítás szerint ekkor , a . def. szerint: . Indukciós lépés: a) eset: az utolsó lépésben a . def. (2) pontját, a tranzitivitást alkalmaztuk, azaz: és . A PSP tételt (. lemma) a feltételre és a indukciós feltételre alkalmazva: . A jobboldal hamis, így a . lemma alkalmazásával azt kapjuk, hogy a baloldal is hamis, azaz: . Az indukciós feltétel szerint: . Beláttuk, hogy , így a . lemma szerint , a . lemma felhasználásával . Az indukciós feltétel szerint: . . lemma alapján: A . def. (diszjunktivitás) alapján: . A . def. (tranzitivitás) kétszeri alkalmazásával: . b) eset: az utolsó lépésben a . def. (3) pontját, a diszjunktivitást alkalmaztuk, azaz: és . Az indukciós feltétel szerint: , amiből a . def. (diszjunktivitás alapján) .

Az összetett program olyan programtulajdonságait is megfogalmazhatjuk, amelyek érvényessége csak olyan változóktól függ, amelyek csak az egyik összetevőben állnak a baloldalon. Az ilyen tulajdonságokat lokálisaknak nevezzük [[???Cha Mis 89]].

Kimondjuk az általános lokalitás tételt ([[???UN 88-93]]/17-90), a bizonyítás Singh, Misra és Knapp bizonyításai alapján a relációs modell eszközeivel is megkonstruálható. A tétel 4. állítása a nyitott specifikáció technikáját alkalmazza.

24.5. Tétel.

(Lokalitás tétel - általános alak) Legyen és közös állapottéren értelmezett program. . Ha , akkor

  • Adjunk meg egy egészértékű variáns függvényt az változóhalmaz érték-n-esei felett. és és .

Biz.: Ha , akkor . Lemma:Misra lokalitási axiómája . Lemma bizonyítása -vel azt a függvénykompozíciót jelöljük, amely a halmazhoz tartozó változókból, mint az állapottér projekciós függvényeiből, a -ben nem szereplő változók helyett az identitásfüggvényből, ill. a logikai függvényből állítható elő. Ha a -hez tartozó függvények értéke változatlan, akkor függvénykompozíció értéke sem változik meg. : Legyen . Ha , akkor , így: . Ha , akkor és , azaz . A . lemma szerint , amelyből ekvivalens átalakítással: , azaz a . def. szerint: .

(1), (2), (3), (4) biz. megtalálható [[???UN 88-93]]-ban. A bizonyítás a most bizonyított lemmára és a , , relációk korábban bizonyított tulajdonságaira épül.

Előző Fel Következő
23.3.Feladatok Tartalom 24.2.Szuperpozíció