Az
program pontosan akkor felel meg az
specifikációs feltételnek, ha van olyan
invariáns tulajdonág, amely mellett megfelel a feltételnek.
-nek).
22.3. Definíció.
Az
program pontosan akkor felel meg az
specifikációs feltételnek a
mellett, ha
.
A program bármely invariáns tulajdonságának igazsághalmaza tartalmazza az elérhető állapotok halmazát (. def., . tétel), így a továbbiakban a . megjegyzésnek megfelelően megengedjük, hogy a program az egyes specifikációs feltételeknek csak egy-egy kiválasztott invariáns tulajdonság igazsághalmaza felett feleljen megEz a döntés megfelel a helyettesítési axiómának [[???Cha Mis 89, ???UN 88-93, ???Pra 94]]. Az alábbiakban megmutatjuk, hogy programok egyes specifikációs feltételekre vonatkozó helyességének bizonyítása során az invariáns tulajdonságokat segédtételként felhasználhatjuk.
22.4. Megjegyzés (Specifikációs feltételek és mindig igaz állítások).
A specifikációs feltételek vizsgálatát megszoríthatnánk egyes mindig igaz állítások igazsághalmazára is, amelyek igazsághalmaza az invariáns tulajdonságokhoz hasonlóan tartalmazza az elérhető állapotok halmazát. A mindig igaz állítások azonban nem használhatóak fel segédtételként az utasítások leggyengébb előfeltételének kiszámítására épülő bizonyítások során. (Ha
mindig igaz, de nem invariáns, akkor
.) A mindig igaz állításokra az sem igaz, hogy szigoríthatóak az átmenetfeltételekre nézve (. . . tétel) [[???Pra 94]].
megfelel a
specifikációs feltételnek, ha van olyan
invariáns tulajdonság ami mellett megfelel a feltételnek.
-nak).
22.5. Definíció.
Az
program pontosan akkor felel meg az
specifikációs feltételnek a
mellett, ha
.
megfelel a
specifikációs feltételnek, ha van olyan
invariáns tulajdonság ami mellett megfelel a feltételnek.
-nak).
22.7. Definíció.
Az
program pontosan akkor felel meg az
specifikációs feltételnek a
mellett, ha
.
22.5. Megjegyzés (Haladási feltételek és az ütemezés).
A definíció a . definícióra épül, amelyben erősen kihasználjuk a feltétlenül pártatlan ütemezés meglétét [[???Cha Mis 89]].
22.8. Definíció (Megfelel
-nak).
pontosan akkor felel meg a
specifikációs feltételnek, ha van olyan
invariáns tulajdonság ami mellett megfelel a feltételnek.
22.9. Definíció.
pontosan akkor felel meg a
specifikációs feltételnek a
mellett, ha
.
pontosan akkor felel meg a
specifikációs feltételnek, ha van olyan
invariáns tulajdonság ami mellett megfelel a feltételnek.
-nak).
22.11. Definíció.
pontosan akkor felel meg a
specifikációs feltételnek a
mellett, ha
.