3.1. példa: Legyen ,
program.
Legyen
továbbá az állítás:
.
Mi lesz a fenti program -hez tartozó leggyengébb előfeltétele?
Megoldás: Írjuk fel először a program programfüggvényét:
Ezek után, a leggyengébb előfeltétel definícióját felhasználva:
,
ugyanis
3.2. példa: Legyen .
Igaz-e, hogy ha minden
programra
, akkor
?
Megoldás: Felhasználva, hogy a leggyengébb előfeltételek minden programra megegyeznek,
egy alkalmas program választásával a válasz egyszerűen megadható: rendelje az
program az állapottér minden eleméhez az önmagából álló egy
hosszúságú sorozatot. Ekkor könnyen látható, hogy tetszőleges
utófeltétel
esetén:
Ekkor viszont
tehát a két feltétel megegyezik.
3.3. példa: Specifikáljuk a következő feladatot:
,
Megoldás:
|
|
|
|
3.4. példa: Legyen ,
program,
egy tetszőleges halmaz.
Legyenek továbbá
és
olyan
relációk, hogy
, valamint
:
Igaz-e, hogy ha , akkor
megoldja
-et?
Megoldás: Próbáljuk meg a megoldás definíciója két pontját belátni. Legyen
. Be kellene
látnunk, hogy
. Nézzük meg a specifikáció tételének bizonyítását: ott felhasználtuk, hogy ekkor van
olyan
, hogy
. Igaz ez a
-re is? Sajnos
– mivel
-t
ősképpel definiáltuk, ez nem feltétlenül van így. Próbáljunk a fenti gondolatmenet
alapján ellenpéldát adni:
Legyen ,
,
,
,
.
Ekkor
és
,
tehát az állítás feltételei teljesülnek függetlenül a programtól (ui.
„hamisból minden következik"). Válasszuk most az alábbi programot:
. Ez a
program nem megoldása a feladatnak, de teljesülnek rá is az állítás feltételei.
Tehát az állítás nem igaz.