Tartalom
Az absztrakt párhuzamos program a UNITY-ből ismert programfogalom relációs alapú megfogalmazása. Ahhoz, hogy eldönthessük, hogy egy program megold-e egy feladatot (. fejezet), össze kell vetnünk a feladatot definiáló relációt a program viselkedését leíró relációval. A programhoz annak viselkedési relációját hozzárendelő leképezést tekinthetjük úgy is, mint egy olyan szemantikai leképezést, amelynek absztrakciós szintje megegyezik az absztrakt feladat szemantikájának absztrakciós szintjével.
Az absztrakt program struktúrája nem eredményezheti, hogy olyan szinkronizációs kényszerek épüljenek be a megoldásba, amelyek feleslegesek, valódi párhuzamos architektúrán szükségtelenül lassítják a program futását. Ha a programot szekvenciális folyamatok halmazának tekintenénk, ahogy ezt pl. CSP-ben [[???Hoa 78]] vagy Adában [[???ALRM 83]] megszoktuk, akkor ezzel eleve végrehajtási sorrendet definiálnánk utasítások nagy részhalmazai felett. Ezért a párhuzamos programot feltételes értékadások halmaza segítségével adjuk meg. Az egyes utasítások bármikor végrehajthatóak, állapotváltozás azonban csak akkor következhet be, ha az értékadás feltétele teljesül. A feltételek helyes megválasztásával elérhetjük, hogy az állapotátmenetek a kívánt sorrendben következzenek be. A program tulajdonságok meghatározását is megkönnyíti, ha a programot utasítások halmazaként definiáljuk. Általában megköveteljük, hogy az egyes értékadások végrehajtása pillanatszerű, atomi legyen.
21.1. Példa (Absztrakt program megadása).
.
Ha az . program utasításainak pillanatszerű végrehajtása
biztosított, akkor az egyik lehetséges végrehajtási út mentén a
következő állapotokat és állapotátmeneteket figyelhetjük meg:
. Ha az értékadások atomicitása nem biztosított, akkor
a következő állapotátmenetsorozat is megfigyelhető:
, pedig nincs olyan érvényes állapot, amelyben
.
A nemdeterminisztikus végrehajtási sorrend korlátozására szinkronizációs feltételeket használunk (pl. termelő-fogyasztó esetén üres pufferből nem lehet fogyasztani). Az absztrakt program tehát szimultán feltételes értékadások (. def.) [[???Fót 83, ???Hor 93]] véges halmazával adható meg [[???Cha Mis 89]], ahol az egyes értékadások jobboldalán függvénykompozíciók is szerepelhetnek (pl. kapcsos zárójellel megadott függvény).
relációt utasításnak nevezzük, ha 
,
.
A
reláció az
utasítás hatásrelációja, ha
ahol
függvény az
véges sorozathoz annak végpontját rendeli.
.
21.3. Definíció.
.
változó konstans függvény 
utasításban, ha 
.
utasítás végrehajtása biztosan nem változtatja meg
változót, ha 
.Elemi utasítás az értékadás és az üres utasítás.
21.4. Definíció (Üres utasítás, SKIP).
Üresnek nevezzük, és SKIP-pel jelöljük azt az utasítást, amire
.
21.5. Definíció (Általános értékadás).
Legyen
,
, ahol
. Az
utasítás általános értékadás [[???Fót 83]] , ha
, ahol az
redukáltjának nevezzük, és
-val jelöljük azt a sorozatot, amit úgy kapunk, hogy az
sorozat minden azonos elemekből álló véges részsorozatát a részsorozat egyetlen elemével helyettesítjük.
Azt mondjuk, hogy a
változó az értékadás baloldalán áll, az értékadás értéket ad a
változónak, ha az
reláció nem egyenlő a
projekcióval [[???Fót 86]], azaz az értékadás hatásrelációja megváltoztatja a
változót (. def.). Az
értékadás baloldalán álló változók halmazát
-sel jelöljük. Az értékadás azoknak a változóknak ad értéket, amelyek a baloldalán állnak A . definíció azokat a változókat nevezi az értékadás baloldalán állónak, amelyek az értékadás végrehajtása során megváltozhatnak, azaz van olyan
állapot, amelyre
. A definíció tehát független az értékadás szintaktikus alakjától..
21.1. Megjegyzés (Szimultán értékadás).
Az értékadás egyszerre több változó értékét is megváltoztathatja, ezért ún. szimultán értékadásról van szó.
21.7. Definíció (Egyszerű értékadás).
Ha legfeljebb egy változó áll az értékadás baloldalán, akkor egyszerű értékadásról beszélünk.
Azt mondjuk, hogy a
változó az értékadás jobboldalán áll, ha az értékadás hatásrelációja nem független (. def.) az
állapottérkomponenstől. Az
értékadás jobboldalán álló változók halmazát
-sel jelöljük.
Legyen
,
, ahol
. Legyen
.
az
kiterjesztése a
feltételre nézve Általánosabban egy
reláció
feltételre vonatkozó kiterjesztését az alábbi módon definiálhatjuk: Legyen
altere
-nak.
. A
függvény az
-beli pontokhoz
-beli vetületüket rendeli hozzá [[???Fót 83]].
.
.:
és
, különben. Az
relációval megadott általános
értékadást feltételes értékadásnak nevezzük, ha
.
21.2. Megjegyzés.
A
változóra vonatkozó egyszerű, determinisztikus, feltételes értékadást a
alakban adjuk meg. Röviden:
-vel jelöljük. Szimultán, nemdeterminisztikus, feltételes értékadás megadható a
alakban. Ha lehetséges, akkor sok változó esetén a
rövidítést alkalmazzuk.
Ha a feltételes értékadásban szereplő valamelyik
egyszerű értékadáshoz rendelt egyetlen feltétel egy
állapothoz
értéket
rendel, akkor ez a . definíció szerint annak a rövid megfogalmazása, hogy az
értékadás az 
pontból indítva nem változtatja meg a baloldalon álló változó
értékét. Ezáltal a feltételes értékadások mindenütt értelmezve
vannak az állapottér felett.