Az állapottér definíciójában szereplő halmazokat típusértékhalmazoknak neveztük, és csak annyit mondtunk róluk, hogy legfeljebb megszámlálhatóak.
A továbbiakban arról lesz szó, hogy ezek a halmazok hogyan jönnek létre, milyen közös tulajdonság jellemző az elemeikre.
Először bevezetünk egy olyan fogalmat, amit arra használhatunk, hogy pontosan leírjuk a követelményeinket egy típusértékhalmazzal, és a rajta végezhető műveletekkel szemben.
5.1. Definíció (TíPUSSPECIfiKáCIó).
A
hármast típusspecifikációnak nevezzük, ha teljesülnek rá a következő feltételek:
: tetszőleges alaphalmaz,
specifikációs invariáns,
a típusértékhalmaz,
, ahol
amelyre
úgy, hogy
és
.
Vegyük észre, hogy az alaphalmaz és az invariáns tulajdonság segítségével azt fogalmazzuk meg, hogy mi az az értékhalmaz, aminek elemeivel foglalkozni akarunk, míg a feladatok halmazával azt írjuk le, hogy ezekre az elemekre milyen műveletek végezhetők el.
Az állapottér definíciójában szereplő típusértékhalmazok mind ilyen típusspecifikációban vannak definiálva. Az állapottér egy komponensét egy program csak a típusműveleteken keresztül változtathatja meg.