Célunk, hogy a modell eszközei segítségével a feladat specifikációját helyettesíteni tudjuk olyan feladatok specifikációival, amely feladatok megoldása esetén a rendelkezésre álló matematikai eszközökkel belátható az eredeti feladat megoldásának helyessége [[???Var 81, ???Fót Hor 91, ???Cha Mis 89, ???Bac Ser 90, ???Mor 87]]. Arra törekszünk, hogy a megoldás előállításával párhuzamosan a megoldás helyességének bizonyítását is előállítsuk.
20.5. Megjegyzés.
A lépésenkénti finomítás szokásos megfogalmazásától eltérően nem a megoldó programot finomítjuk [[???Bac Ser 90]]Egy program finomítása egy másiknak, ha minden olyan specifikációnak megfelel, amelyiknek az eredeti program is megfelelt [[???Bac Ser 90]].. A feladat finomításának elve különbözik Morris [[???Mor 87]], ill. Lamport [[???Lam 91]] felfogásától is, mert ezekben a modellekben magát a programot is specifikációs eszköznek tekintik és ennek megfelelően finomítják a specifikációt.
A specifikáció finomításának leggyakoribb módja az állapottér bővítése, a régi és új komponensekre további, általában a korábbiaknál szigorúbb feltételek megfogalmazása.
Azt, hogy egy feladat mikor finomítása egy másiknak egy rögzített állapottér felett, a program (. def.) és a megoldás (. def.) definíciójának felhasználásával indirekt úton adjuk meg. Ez a definíciós módszer alkalmas arra, hogy a feladatok lépésenkénti finomítása során az egyes lépéseink helyességét formálisan is igazoljukA programok felett értelmezett finomítás reláció is a megoldás fogalmához kötött [[???Bac Ser 90, ???Mor 87]], és a finomítást támogató kalkulus alapja.. A feladatok felett értelmezett finomítás relációt tehát a feladatok és programok között értelmezett megoldás reláció indukálja.
20.4. Definíció (Feladat finomítása).
Azt mondjuk, hogy az
feladat finomítása az
feladatnak, ha minden olyan
program, ami megoldása az
feladatnak az megoldása az
feladatnak is.
20.3. Példa (Feladat finomítása).
Az alábbi specifikáció finomítása a (.)-(.) feltételekkel megadottnak.
ahol
elemenként feldolgozható.
Annak bizonyítása, hogy a fenti specifikáció valóban finomítása a (.)-(.) feltételekkel megadottnak megtalálható a . fejezetben.
Azt mondjuk, hogy az
feladat ekvivalens az
feladattal, ha az
finomítása az
-nek és az
finomítása az
-nek.
20.6. Megjegyzés (Absztrakt feladat).
Nevezzük a most bevezetett ekvivalenciareláció által létrejött ekvivalenciaosztályokat absztrakt feladatnak. A most bevezetett ekvivalenciareláció indukál egy homomorfizmust a feladatokról az absztrakt feladatokraKét absztrakt feladat pontosan akkor különbözik egymástól, ha az egyikhez található olyan megoldás, amelyik a másiknak nem megoldása. .
Négyféle módon finomítjuk a feladat matematikai modelljét:
az állapottér komponenseit finomítjuk és mint altereket tekintjük őket,
az állapottér alterein fogalmazunk meg feladatokat,
az állapotteret további komponensekkel bővítjük, a hozzájuk tartozó változókra kikötéseket teszünk,
állapottér transzformációt [[???Fót 86]], vagy más néven koordinátatranszformációt [[???Dij Sch 89]] alkalmazunk.
20.7. Megjegyzés.
Ha el akarjuk dönteni, hogy egy feladat finomítása-e egy másiknak abban az esetben, amikor a két feladat állapottere különbözik, akkor a két feladat állapotterét feleltessük meg egy kiválasztott állapottér egy-egy alterének és adjunk meg egy-egy olyan függvényt, amelyik a kiválasztott altér hatványhalmazára a feladat állapotterének hatványhalmazát leképezi. Ezek a leképezések definiálják a feladatok megfelelőit az új állapottér alterein. A feladatokat ezek után kiterjeszthetjük a közös állapottérre. Legtöbbször a választott állapottér a két feladat egyikének állapottere, a másik feladat állapottere a közös tér egy altere, a leképezés pedig az identitás.
20.8. Megjegyzés.
Feladatok specifikációjának finomításakor támaszkodunk a nyitott specifikáció technikájára. Az állapottér egy alterén definiált részfeladat környezeti feltételeiként olyan biztonságossági-, haladási- és fixpontfeltételeket adunk meg, amelyek az altér felett specifikált komponens és környezete által együttesen alkotott zárt rendszertől [[???Jär 92]] elvárt viselkedésre vonatkoznak (. fejezet) [[???Col 94, ???Cha Mis 89]]. Az alterekre vonatkozó feltételeket megkülönböztetésül felső indexszel jelöljük, pl.:
,
,
,
. A részfolyamat egyes tulajdonságainak vizsgálatakor felhasználjuk a teljes rendszer (a külső környezet) ismert vagy feltételezett tulajdonságait [[???Cha Mis 89, ???Col 94]].
A lépésenkénti finomítás során újabb és újabb részletekkel egészítjük ki a specifikációt, majd az utolsó lépésben előállítjuk a megoldó programot. A program előállítása általában egyszerű, a specifikáció finomítása nehezebb feladat. Minden egyes lépés után igazolnunk kell, hogy az új és részletesebb specifikációt megoldó program megoldja az eredeti feladatot is. A specifikáció finomítása során építjük be a megoldásba mindazt a tudást, amelyet a feladat elemzése során, vagy korábban szereztünk. A finomítás iránya kisebb vagy nagyobb mértékben befolyásolja, hogy milyen architektúrán implementálható hatékonyan a kapott megoldás és melyiken nem. Ezért akárcsak a szekvenciális programok levezetése során, a párhuzamos programok fejlesztésekor is előfordulhat, hogy visszatérünk egy korábban megfogalmazott specifikációhoz és más irányban folytatjuk a specifikáció finomítását.