Vizsgáljuk meg, hogy a típusspecifikációban leírt követelményeket hogyan valósítjuk meg. Ehhez bevezetjük az elemi típusértékek halmazát, amit -vel jelölünk.

A típus első két komponense az absztrakt adattípus reprezentációját írja le, míg a programhalmaz a típusműveletek implementációját tartalmazza.

Meg kell még vizsgálnunk azt a kérdést, hogy mikor mondjuk, hogy egy típus megfelel a típusspecifikációnak, azaz a típus mikor teljesíti a specifikációban leírt követelményeket.

Természetesen a megfelelés definíciója még nem teljes, meg kell még mondanunk, hogy mit értünk a -n keresztüli megoldáson. Ehhez először vizsgáljunk meg egy egyszerű esetet: tegyük fel, hogy a feladat és a program állapottere egykomponensű.

Persze a fenti definíciók figyelembe vételével ez azt jelenti, hogy a feladat állapottere , a programé pedig . Ekkor tulajdonképpen a -n keresztüli megoldást úgy kell elképzelni, mintha a megoldás definíciójában a programfüggvény reláció lenne, azaz

Legyen a továbbiakban , és , , , , . Azt mondjuk, hogy az állapottér illeszkedik az állapottérhez, ha

A fenti esetben legyen a leképezés az alábbi módon definiálva:

ahol , és

A továbbiakban az ilyen felépítésű relációt -nel fogjuk jelölni. Vegyük észre, hogy a tulajdonképpen a egyfajta kiterjesztése több komponensű, de egymáshoz illeszkedő állapotterek esetén. Ezek után a megoldás definícióját felírhatjuk az ilyen esetre úgy, hogy az előző megoldásdefinícióban helyére -t írunk.

Most már csak egy kis lépés van hátra az általános eset leírásához: ha a program és a feladat állapottere nem illeszkedik egymáshoz, akkor tegyük illeszkedővé őket. Ez a kiterjesztés fogalmának felhasználásával könnyen megtehető.

Természetesen egy típusspecifikációnak több különböző típus is megfelelhet. Ekkor az, hogy melyiket választjuk a reprezentáció és a műveletek implementációinak más további tulajdonságaitól – ilyen például a reprezentáció memóriaigénye, vagy az implementációk műveletigénye – függ. Ez a döntés mindig a megoldandó programozási feladat függvénye.