Az eddig elmondottakból alapján a specifikáció tétele még nem lenne hatékonyan használható, hiszen a paramétertér minden pontjára ellenőriznünk kellene a feltételek teljesülését. Ezért bevezetjük a változó fogalmát, aminek segítségével a feltételrendszer teljesülése egyszerűbben ellenőrizhetővé válik.

A változók használatával egyszerűsíthetjük az állapottéren értelmezett állítások (elő- és utófeltételek, leggyengébb előfeltétel) és relációk (programfüggvény) leírását.

Mivel minden változó értelmezési tartománya az állapottér és értékkészlete egy típusértékhalmaz, egy változót jellemezhetünk egy típussal, azaz beszélhetünk a változó típusáról.

Ha a paramétertér is direktszorzat alakú – márpedig ez gyakran így van, ugyanis általában az állapottér egy altere – akkor a paramétertér egydimenziós projekciós függvényeit paraméterváltozóknak nevezzük.

Az állapottér illetve a paramétertér egyes komponenseihez a változókat, illetve paraméterváltozókat az adott komponens alá írjuk.

Most megvizsgáljuk, hogyan lehet a specifikáció tétele segítségével feladatokat megfogalmazni.

Tekintsünk egy már ismert feladatot: határozzuk meg két egész szám összegét!

Először felírjuk az állapotteret, úgy mint eddig, csak kiegészítjük a változó nevek megadásával.

Az eddigi jelöléseink alkalmazásával a feladat

A specifikáció tétele alkalmazásához írjuk föl a paraméterteret is:

Majd még visszatérünk arra, hogy miért éppen így választottuk meg a paraméter teret.

Tehát az állapottér három egész komponensből áll, melyeknek változói rendre , és . A paramétertér két egész komponensből áll, az első komponens változója , a másodiké .

Legyen az reláció a következő:

pedig

A fentiekből adódik, hogy . A paramétertér egy tetszőleges eleméhez tartozó elő- és utófeltételre:

amit az állapottér és a paramétertér változóinak felhasználásval is fölírhatunk:

A függvénytereknél tárgyaltuk, hogy a függvénytér elemein a relációk egy logikai függvényekből álló teret generálnak. egy függvénytér elemei, szintén annak tekinthetők, konstans függvények. Ezért és az állapottéren értelmezett logikai függvények, ahogy is az. Ebből következik, hogy

és mivel minddegyik függvény,

A jelölés egyszerűsíthető, mivel nyílvánvaló, hogy a paraméter változók argumentuma , ezek el is hagyhatók, sőt, általában az sem okoz félreértést, ha az elő- utófeltételek indexeit elhagyjuk. Ezek a feltételek a paramétertér pontjaihoz tartoznak és így a paraméterváltozók értékeitől függnek. A feladat specifikációja tehát:

A továbbiakban a feladatot úgy definiáljuk, hogy megadjuk az állapotterét ( ), a paraméterterét ( ), valamint az elő- és utófeltételét ( illetve ) a paramétertér minden pontjára, azaz paraméteresen. Ebben az esetben azt mondjuk, hogy a feladatot megadtuk a specifikáció tételének megfelelő formában, vagy ha nem okoz félreértést, specifikáltuk a feladatot.

Egy feladatot nagyon sokféleképpen lehet specifikálni, a sok lehetőség közül az egyik az, amit elő-, utófeltétellel történő specifikációnak szoktak nevezni és nagyon hasonlít arra, amit most tárgyalunk. Felhívjuk a figyelmet, hogy a hasonlóság ellenére a kettő nem azonos.

Paramétertérnek általában az állapottér egy alterét szoktuk választani. Azokat a komponenseket válogatjuk ki, amelyek értékétől függ, hogy a feladat mihez, mit rendel, amik paraméterezik a feladatot. Lényegében azt fogalmazzuk meg, hogy az állapottér milyen tulajdonságú pontjaiból, milyen tulajdonságú pontokba akarunk jutni. A paraméterteret arra használjuk, hogy megadjuk milyen összefüggés van az elérendő és a kiinduló állapotok között.

Ha egy programnak meg tudjuk határozni a (paraméteres) utófeltételhez tartozó leggyengébb előfeltételét, akkor a specifikáció tétele alapján, könnyen eldönthetjük, hogy megoldása-e a specifikált feladatnak, más szóval bebizonyíthatjuk a program helyességét. Megjegyezzük azonban, hogy legtöbbször a "fordított" utat fogjuk követni, nem a program helyességét bizonyítjuk, hanem bizonyítottan helyes programot állítunk elő.

A későbbiekben bevezetünk majd olyan eszközöket, amelyek segítségével a feladat specifikációjából kiindulva olyan programokat készíthetünk, amelyek megoldják a feladatot.