-nek)
megfelel
specifikációs feltételnek, ha van olyan
, hogy
és
.
Biz.: . és . definíciók közvetlen következménye.
22.1. Következmény.
megfelel
specifikációs feltételnek, ha
és
és
.
22.2. Tétel.
(Megfelel
-nak
mellett) Az
program pontosan akkor felel meg a
specifikációs feltételnek, ha megfelel a legszigorúbb invariáns mellett, azaz, ha
mindig igaz (
).
Biz.: Ha megfelel a legszigorúbb invariáns mellett, akkor van olyan invariáns,
amely mellett megfelel, így a . definíció szerint megfelel a feltételnek. Ekkor
.
a legszigorúbb
invariáns, így: 
, azaz 
mindig igaz.
Ha megfelel a feltételnek, akkor van olyan
invariáns
amely mellett megfelel, így a . tétel szerint a legszigorúbb invariáns szerint is megfelel
a feltételnek. 
(Megfelel
-nak)
megfelel a
specifikációs feltételnek a
invariáns tulajdonság mellett, ha
. Biz: A .,. definíciók közvetlen következménye.
(Megfelel
-nak
mellett) Az
program pontosan akkor felel meg a
specifikációs feltételnek, ha megfelel a legszigorúbb invariáns mellett, azaz:
.
Biz.: Ha megfelel a legszigorúbb invariáns mellett, akkor van olyan
invariáns, amely mellett megfelel, így a . definíció szerint
megfelel a feltételnek. Ha megfelel a feltételnek, akkor van olyan
invariáns
amely mellett megfelel, így a . tétel szerint a legszigorúbb invariáns szerint is megfelel
a feltételnek. 
22.6. Megjegyzés.
Azt mondjuk, hogy
megfelel a
stabil
feltételnek, ha megfelel a
feltételnek.
22.5. Lemma.
(Megfelel
-nak) Az
program megfelel
specifikációs feltételnek a
invariáns tulajdonság mellett, ha
megfelel a
feltételnek
mellett, és
.
Biz.: . . definíciók és a . lemma közvetlen következménye.
(Megfelel
-nak
mellett) Az
program pontosan akkor felel meg a
specifikációs feltételnek, ha megfelel a legszigorúbb invariáns mellett, azaz:
.
Biz.: . tétel bizonyításához hasonlóan a . tétel felhasználásával.
(Megfelel
-nak
mellett) Az
program pontosan akkor felel meg a
specifikációs feltételnek, ha megfelel a legszigorúbb invariáns mellett, azaz:
.
Biz.: . tétel bizonyításához hasonlóan a . tétel felhasználásával.
22.8. Lemma.
(Megfelel
-nak
mellett) Az
program pontosan akkor felel meg a
specifikációs feltételnek, ha
.
Biz.: Ha 
, akkor a . tétel miatt (a legszigorúbb invariáns stabil):
. Az állítást az előző tétel alkalmazásával kapjuk. Ha
megfelel
-nak, akkor az előző
tétel szerint 
. A . lemma
szerint a 
jobboldala
gyengíthető, így 
. 
22.2. Következmény.
Az
program pontosan akkor felel meg a
specifikációs feltételnek, ha
. Biz.: A . tétel szerint
.
-nak
mellett)
program pontosan akkor felel meg a
specifikációs feltételnek, ha
.
Biz.: A .,.,. def. és . lemma közvetlen következménye.
22.10. Lemma.
(Megfelel
-nek)
megfelel a (
) specifikációs feltételnek az
állapottér felett, a
invariáns mellett, ha
, ahol a
logikai függvény az
program
feletti fixpontjainak halmazát adja meg (. def.).
Biz.: A . és a . def. közvetlen következménye.
-nek 
mellett)
pontosan akkor felel meg a (
) kikötésnek, ha 
.
Biz.: Az előző lemma következménye.
22.7. Megjegyzés (Megoldás
mellett).
Ha
megoldja a feladatot egy
invariáns tulajdonság mellett, akkor
megoldja a feladatot. Ha
megoldja a feladatot, akkor megoldja a legszigorúbb invariáns mellett is.
22.12. Tétel.
(Program és feladat kiterjesztése) Legyen az
feladat és az
program az
állapottér
altere felett definiálva. Ha
megoldja
-et, akkor
kiterjesztése
-ra megoldja az
feladat
-ra való kiterjesztését A tétel a [[???Fót 88]] cikk egyik kiterjesztési tételének általánosítása. A többi kiterjesztési tétel megfelelője is megfogalmazható..
Biz.: A . def. szerint az 
program viselkedési relációja a megoldás definíciója szerint tartalmaz
minden olyan programtulajdonságot, amely ahhoz szükséges, hogy
megfeleljen
az 
specifikációs feltételeinek. A programtulajdonságok mindegyikének
definíciója a leggyengébb előfeltételre épül, ezért . def. és a .
lemma szerint a programtulajdonságok kiterjesztései tulajdonságai
a kiterjesztett programnak is. Így a kiterjesztett feladat (. def.)
specifikációs feltételeinek kielégítéséhez szükséges valamennyi
programtulajdonság szerepel a kiterjesztett program viselkedési relációjában.
invariáns tulajdonság mellett