3.4Példák

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.