Tartalom
invariáns tulajdonság mellett
Megadjuk, hogy egy absztrakt program mikor old meg egy feladatot. A megoldás fogalmát a leggyengébb előfeltétel fogalmára építjük fel. A megoldás definíciója így egy olyan verifikációs kalkulus alapja, amely helyes program esetén a specifikációs feltételek és az absztrakt program utasításainak számával lineárisan arányos számú lépésben véget ér. Kimondunk néhány tételt, amelyek a verifikációt egyszerűsítik, illetve igazolják, hogy a bevezetett megoldásfogalom megfelel elvárásainknak.
22.1. Definíció (Megoldás).
Azt mondjuk, hogy az
program megoldja az
feladatot (. def.), ha
, hogy az
program megfelel a
-ban adott
,
,
,
,
,
alakú specifikációs feltételek mindegyikének a
kezdeti feltételek mellett.
Az alábbiakban sorra megadjuk, hogy egy
program mikor felel meg az egyes specifikációs feltételeknek a
kezdeti feltételek mellett.
22.1. Megjegyzés (Specifikációs feltételek és elérhető állapotok).
Rögzített program esetén indokolt a specifikációs feltételek vizsgálatát az elérhető állapotok halmazára korlátozni [[???Lam Lyn 90, ???San 91, ???Pra 94]]. Ha a program megfelel egy specifikációs feltételnek az elérhető állapotok felett, akkor a specifikációs feltétel nem sérül a program futása során. A gyakorlatban azonban általában az elérhető állapotok halmazánál tágabb halmazt választunk (v.ö.: . megjegyzés), szélső esetben akár az összes állapotot, a teljes állapotteret is figyelembe vehetjük.
22.2. Megjegyzés.
A megoldás definíciójának megadásakor az absztrakt program viselkedési relációjának bekezdésben adott definíciójára (. def.) támaszkodunk az absztrakt program (. def.) definíciója helyett. A viselkedési reláció és a feladat hasonló szerkezetű, így könnyen összehasonlíthatóak.