Legyen
egy állapottér,
pedig egy tetszőleges, megszámlálható halmaz. Rendeljünk hozzá a
pontokhoz rendezett reláció heteseket. Minden egyes rendezett hetes kettő, peremfeltételeket megadó, illetve öt, átmenetfeltételeket leíró relációt tartalmaz. Az
relációt az
állapottér felett definiált feladatnak,
-t pedig a feladat paraméterterének nevezzük. A
és
direktszorzat
-hez rendelt
elemének komponenseit rendre
,
,
,
,
-val jelöljük. Ha
egyelemű, akkor
helyett
-t írunk vagy a
indexet teljesen elhagyjuk, ha ez nem okoz félreértést.
20.2. Példa (Programozási feladat).
Példaként megadjuk az elemenkénti feldolgozás feladatának specifikációját: A specifikációs relációk közül négy üres, három pedig egyelemű. Kikötjük, hogy bármely fixpontban az
rendezett halmaz-
-es értéke éppen
legyen ((.) feltétel), ahol
az
változó kezdeti értéke ((.) feltétel). Megköveteljük, hogy a program biztosan elérje valamelyik fixpontját ((.) feltétel). A feladat megfogalmazásában az
függvény argumentuma, mint a specifikációs feltételek paramétere jelenik meg.
,
.
ahol
elemenként feldolgozható.
Az
típus specifikációja, az elemenként feldolgozható függvény fogalma és a megoldó program megtalálható a . fejezetben.
A paramétertér helyes megválasztásával elérhetjük, hogy a
,
,
, stb. relációk
végesek legyenek, vagy éppen csak egyetlen egy halmaz ill. halmazpár legyen az
elemük. Ha a 
paramétertér végtelen, akkor így összességében végtelen sok
relációt adunk meg. Ezek a relációk azonban általában csak a
paraméter
értékében különböznek egymástól, így a megoldás definícióját elegendő
lesz egyetlen 
paraméteres esetre megvizsgálni.
A paramétertér bevezetésével könnyen megfogalmazhatunk olyan
feladatokat, amelynek megoldása több alternatív viselkedésminta szerint is
lehetséges Ha a feladat determinisztikus, akkor megfogalmazhatnánk
a feladatot a paramétertér bevezetése nélkül is, mint a
direktszorzat elemét. Ebben az esetben azonban a feladat egyes komponenseinek
számossága kezelhetetlenül nagy lehet, pl. egy-egy átmenetfeltételnek
általában végtelen sok halmazpár eleme lenne..
20.2. Megjegyzés.
A paramétertér általában maga is az állapottérhez hasonló direktszorzat. Sok esetben van az állapottérnek és a paramétertérnek nem üres, közös altere. A paramétertér projekcióit is változóknak nevezzük, ezeket a változókat megkülönböztetésül
jellel egészítjük ki, pl.:
.Elsőrendű temporális logikai nyelvekben szokás az állapottér változóit lokális változóknak, a paramétertér változóit globális vagy rigid változóknak nevezni.
20.3. Megjegyzés.
A feladat fenti definíciója a [[???Fót 83, ???Fót Hor 91]]-ben ismertett specifikációs módszer általánosítása. Legyen
és
,
és
.
20.4. Megjegyzés.
A specifikációs feltételek szintaktikus alakjától a feladat, mint reláció független. Lényegében ugyanazt a feladatot (. def.) azonban több ekvivalens specifikációs feltételhalmazzal is megfogalmazhatjuk.
Az . definícióban megadjuk, hogy az
feladatnak
mikor megoldása egy program, azaz mikor elégíti ki a feladatban előírt
feltételeketAzt mondjuk, hogy az 
program megoldja az 
feladatot, ha 
,
hogy az 
program
megfelel a 
-ban adott 
,
,
,
,
,
alakú specifikációs feltételek mindegyikének a
kezdeti feltételek mellett..