23.1. Feladat.
Legyen
egy természetes szám!
Vizsgáljuk meg, hogy az alábbi program megfelel-e a fenti specifikációnak?
{
}
23.2. Feladat.
Legyen
, és
tetszőleges természetes szám. Legyen
monoton növekedő függvény.
, ahol
.
Vizsgáljuk meg, hogy az alábbi program megfelel-e a fenti specifikációnak?
{
}
23.3. Feladat.
,
,
Spec. 1.
Spec. 2.
Igaz-e, hogy a - specifikáció finomítása a feltételnek? Igaz-e, hogy az alábbi program megoldja a - feltételekkel és a
variánsfüggvény bevezetésével finomított feladatot?
23.4. Feladat.
,
,
Spec. 1.
ahol
azon vektorok halmaza, amelyeket
-ból az
elemeinek permutálásával kapunk,
. Spec. 2. Bővítjük az állapotteret
-nel.
Igaz-e, hogy a - specifikáció finomítása a feltételnek? Igaz-e, hogy az alábbi program megoldja a - feltételekkel és a
variánsfüggvény bevezetésével finomított feladatot?
ahol
és
Igaz-e, hogy
?
23.5. Feladat.
Adottak az
függvények, melyekre:
(Hasonlóan
-re illetve
-ra is.)
Legyen továbbá
a következő:
Tekintsük a következő specifikációt:
Igaz-e„ hogy a következő program megfelel a fenti specifikációnak:
INIT:
23.6. Feladat.
Adott az
vektor, amelynek elemei természetes számok.
. Rendezzük az
vektort növekvően!
a) Írjuk fel a feladat specifikációját!
b) Bizonyítsuk be, hogy a következő program megfelel a specifikációnak:
23.7. Feladat.
Feladat: számoljuk ki a Pascal háromszög első N sorát (a 0-tól az N-ig)!
Specifikáció:
Az invariáns finomítśához használjuk fel:
Fejezzük be a specifikációt, majd lássuk be, hogy az alábbi program megoldja a feladatot, ill. megfelel a specifikációnak! A fenti specifikációhoz adott a program:
