Az, hogy a most megadott típus megfelel a fenti típusspecifikációnak, könnyen látható: a reprezentáció helyessége a és az definíciójából leolvasható, míg az, hogy az program a -n keresztül megoldja az feladatot, a program egyszerű hozzárendeléséből és a „trükkös" megválasztásából látszik.

Természetesen másmilyen reprezentációs függvényt is meg lehet adni, de ekkor meg kell változtatnunk a típusinvarinánst és a programot is.

5.2. példa: Specifikáld azt a típust, melynek értékei a halmaz részhalmazai, típusműveletei pedig két részhalmaz metszetének ill. uniójának képzése, ill. annak megállapítása, hogy egy elem eleme-e egy részhalmaznak. Adj meg egy típust, amely megfelel a specifikációnak! (Az elemi értékek halmaza: , a programokat elég a programfüggvényükkel megadni.)

Megoldás:  , ahol

és ,

Adjunk a fenti specifikációnak megfelelő típust! , és ,

és program

program

program

Vajon megfelel a most leírt típus a fenti típusspecifikációnak? A reprezentáció helyes, ugyanis a pontosan 128 hosszú sorozatokat a reprezentációs függvény éppen a kívánt részhalmazokba képezi le, azaz

Vizsgáljuk meg a programok és a feladatok viszonyát. Vegyük észre, hogy a programok állapotterei illeszkednek a megfelelő feladat állapotteréhez, tehát felírható közöttük a reláció.

Ezek felhasználásával a -n keresztüli megoldás egyszerűen adódik a reprezentációs függvény és a programfüggvények szemantikájából.

5.3. példa: Legyen egy típusspecifikáció, . Legyenek és típusok, melyekre: , és .

Igaz-e, hogy ha megfelel -nek, akkor is?

Megoldás: A reprezentáció helyessége és miatt triviálisan teljesül, hiszen ekkor:

Azt kell tehát megvizsgálnunk, hogy vajon az program megoldja-e az feladatot a -n keresztül. Mivel a programok állapottere közös, feltehetjük, hogy a programok állapottere és a feladat állapottere egymásnak megfeleltethető, hiszen ellenkező esetben mindkét megoldás-vizsgálatnál a feladatnak ugyanazt a kiterjesztését kellene használnunk, és így az eredeti feladatot ezzel a kiterjesztéssel helyettesítve az alábbi gondolatmenet végigvihető.

Mivel , a két program programfüggvényére teljesül a következő:

Jelöljük most is -val a program és a feladat állapottere közötti, a megfeleltetésben definiált leképezést. Könnyen látható, hogy az tulajdonság miatt

Másrészt mivel az program megoldja -et a -n keresztül

is teljesül. A fenti két állítás alapján

Használjuk fel a második tulajdonságot is! Az tulajdonság miatt igaz az alábbi állítás is:

Ekkor viszont mivel az program – a -n keresztül – megoldása a feladatnak, teljesül, hogy

és ezért

azaz az program is megoldja az feladatot a -n keresztül, tehát a típus is megfelel a specifikációnak.