Tartalom
A feladat definíciójának megfogalmazásakor általánosítjuk azt a specifikációs módszert, amely relációk segítségével megfogalmazott elő- és utófeltételeket használ. A most bevezetett feladatfogalom magában foglalja azt az esetet is, amikor egy vagy több nem feltétlenül termináló folyamat, egy zárt rendszer együttes viselkedésére teszünk előírásokat. Megjegyezzük, hogy a feladat függetlenül megfogalmazható bármely lehetséges megoldásától, összehasonlítható más feladatokkal, illetve összevethető tetszőleges vele közös állapottéren futó programmal abból a szempontból, hogy az megoldja-e. A feladat megoldása nem feltétlenül csak párhuzamos program lehet.
A könyv első részében bevezetett feladat fogalmát általánosítjuk, hogy olyan feladatokat is specifikálhassunk, amelyek elő- és utófeltételek segítségével nem írhatóak le. Ilyen feladat például egy operációs rendszer feladata, amelynek folyamatos helyes működésében vagyunk érdekeltek egy utófeltétel teljesülése helyett. Folyamatszabályozó szoftverek, beágyazott rendszerek működése is biztonságossági, haladási feltételekkel jellemezhető utófeltételek megadása helyett.
A feladat matematikai megfelelője specifikációs relációk együttese. A specifikációs relációkat az állapottér hatványhalmaza felett értelmezzük, a relációk elemeit specifikációs feltételeknek nevezzük.
A specifikációs feltételek a programra, mint az állapottér feletti mozgásra fogalmaznak meg kikötéseket. Ezeket a kikötéseket csoportosíthatjuk típusuk szerint. Egy feladat leírásához hét féle feltételt használunk. Az azonos feltételtípushoz tartozó feltételeket egy relációban gyűjtjük össze, így hét specifikációs relációt vezetünk be.
Legyen 
logikai függvény.
relációk,
és 
halmazokunáris relációk.
A relációk megadásakor infix jelölést alkalmazunk, ezért bevezetjük az alábbi jelöléseket. Zárójelben megadjuk azt is, hogy hogyan olvassuk azt, ha egy halmaz vagy egy halmazpár eleme az adott relációnak. Az állapottér részhalmazait logikai relációkkal jellemezzük.
Jelölések:
(
stabil feltéve,
hogy nem 
), 
(
biztosítja 
-t), 
(
-ből
elkerülhetetlen 
), 
(
-ból a program biztosan fixpontba jut),
(
teljesül fixpontban), 
(
invariáns). 
(
igaz
kezdetben), 20.1. Példa (Specifikációs reláció).
Legyen az állapottér
egyelemű direkt szorzat. Az egyetlen komponenshez tartozó változót jelöljük
-vel. Legyen
. Ekkor pl. az
feltétel azt a kikötést fogalmazza meg, hogy a program az
állapotból csak az
állapotba juthat. A teljes reláció azt a feltételegyüttest adja meg, amely megköveteli, hogy a program futása során az
változó értéke csak egyesével növekedhet. Megkönnyíti a relációk kezelését, ha egy-egy relációnak csak néhány eleme van. Ezért célszerű a reláció
paraméter szerinti felbontása egyelemű relációkra, erre a célra vezetjük majd be a paramétertér fogalmát.
A programra, mint az állapottér feletti mozgásra vonatkozó specifikációs feltételeket négy csoportra osztjuk aszerint, hogy milyen típusú kikötéseket fogalmazunk meg segítségükkelA kikötések teljesülését - az invariánsok kivételével - általában nem a teljes állapottér felett vizsgáljuk majd meg, hanem csak az állapottér egy olyan részhalmaza felett, amely tartalmazza az összes elérhető állapotot.. A relációcsoportok és az egyes specifikációs relációk elnevezései azt tükrözik, hogy az adott reláció segítségével milyen jellegű feltételeket kívánunk megfogalmazni. A specifikációs relációk pontos szemantikáját az adja meg, hogy egy program mikor felel meg egy adott relációhoz tartozó feltételnek. Ennek megfogalmazásához szükséges az absztrakt program (. def.) és a megoldás (. def.) definíciójának ismereteA feladat szemantikáját a specifikációs relációk segítségével meg tudjuk adni oly módon, hogy bármely feladat függetlenül leírható bármely azt megoldó vagy meg nem oldó programtól, azaz a feladatok a programoktól független szemantikával rendelkeznek a modellben.. Az alábbiakban röviden és informálisan már most megadjuk az egyes feltételek jelentését.
A
és az 
alakú feltételeket biztonságossági feltételeknek nevezzük. Ha a
program állapotára teljesül a 
feltétel, akkor 
tiltja, hogy a program 
érintése nélkül közvetlenül egy 
-beli állapotba jusson. 
pedig kiköti, hogy a 
feltétel igazsághalmazából a program minden elemi lépése a
igazsághalmazába vigyen, valamint, hogy 
„kezdetben”A kezdeti értékadás végrehajtása után.
is teljesüljön.
A
, illetve 
haladási feltételek előírják, hogy ha a program egy 
-beli állapotba jut, akkor abból előbb - utóbb 
-ba jusson. 
további megszorítást tesz a haladási irányra. 
kikötésnek megfelelő program előbb-utóbb biztosan fixpontba jut
-beli állapotából.
A
fixpont feltételekkel szükséges feltételeket fogalmazunk meg arra,
hogy a program fixpontba jusson.
Elégségesnek tekintjük, ha
kezdeti feltételekkel meghatározott állapotokból indítva helyesen
működik a program.
20.1. Megjegyzés.
Stabilitási feltételnek nevezzük
-t , ha
.
konstans feltétel, ha
is és
is stabilitási feltétel.
A továbbiakban a 
relációkat specifikációs relációknak, elemeiket specifikációs feltételeknek, ezen
belül az 
,
,
,
,
relációk elemeit
átmenetfeltételeknek, az 
relációk elemeit pedig peremfeltételeknek nevezzük. Az
reláció a környezeti előírások csoportjába tartozik.