Egy program szemantikai jelentését azonosíthatjuk az általa az állapottér hatványhalmaza felett definiált - invariánsok, biztonságossági, haladási, fixpont és terminálási tulajdonságoknak megfelelő unáris és bináris - relációk együttesével. Egy ilyen szemantika leíró jellegűLeíró szemantikáról csak akkor beszélhetünk, ha a szemantikus leképezés kompozícionális. A kompozcionalitás azonban csak részben teljesül a modellben (. fejezet), amely általában elegendő ahhoz, hogy a megoldást részfeladatok megoldásából programkonstrukciók segítségével előállítsuk, de nem felel meg a kompozicionalitás szigorú matematikai követelményének. (. fejezet) [[???Jut Kna Rao 89]] és absztrakciós szintje lényegében megegyezik a bevezetett megoldásfogalom absztrakciós szintjével.