A típusspecifikáció és a típus fogalmának bevezetésével tulajdonképpen a feladat fogalmát általánosítottuk, míg a megfeleltetés a megoldás fogalmának volt egyfajta általánosítása. Az imént megismert specifikáció tétele a megoldásra adott elégséges feltételt. Próbáljunk most a -n keresztüli megoldásra egy hasonló feltételt adni!

5.1. TéTEL: TíPUSPECIfiKáCIó TéTELE Legyen és adott típusspecifikáció és típus, és tegyük fel, hogy a reprezentáció helyes, azaz . Legyen továbbá , az állapottere , egy paramétertere , elő és utófeltétele pedig és . Legyen és tegyük fel, hogy állapottere illeszkedik állapotteréhez. Definiáljuk a következő állításokat:

ahol a program és a feladat állapottere közötti, a -n keresztüli megoldás definíciójában szereplő leképezés. Ekkor ha akkor az program a -n keresztül megoldja az feladatot.

Bizonyítás:  A -n keresztüli megoldás definíciója két pontjának teljesülését kell belátnunk:

_

Az, hogy a fenti tétel feltételei között kikötöttük, hogy a program állapottere illeszkedik a feladat állapotteréhez tulajdonképpen elhagyható. Ekkor a tétel a feladat és a program olyan kiterjesztéseire mondható ki, amelyek állapotterei illeszkednek egymáshoz (pontosan úgy, ahogy a megfeleltetést definiáltuk nem illeszkedő állapotterek között).

A következő példában megmutatjuk, hogy -t gyenge igazsáhalmaz helyett erős igazsághalmazzal definiálnánk, akkor a tétel nem lenne igaz.

Legyen , , , . Legyen állapottere és a paramétertér is legyen ugyanez: . Legyen specifikációja:

Ekkor és . Legyen továbbá az elemi értékek halmaza , , , és az egy hosszú sorozatokra:

Tegyük fel, hogy , , és rendelje az állapottere minden pontjához az önmagából álló egy hosszú sorozatot. Ennek a programnak az állapottere illeszkedik a fenti feladat állapotteréhez, és . Ekkor

tehát

Az viszont könnyen látható, hogy

tehát a típus nem felel meg a specifikációnak.