Tartalom
A továbbiakban bizonyos speciális függvények helyettesítési
értékének kiszámításával fogunk foglalkozni. Tegyük fel, hogy van egy
függvényünk,
ahol 
és 
tetszőleges halmazok. A feladat specifikációja tehát:
|
|
|
|
Természetesen ha semmi mást nem tudunk a függvényről, akkor a fenti specifikációhoz nem tudunk igazi megoldóprogramot adni. Ezért az elkövetkezőkben további feltételezésekkel fogunk élni.
Tegyük fel, hogy 
, ahol 
és 
függvények.
Tétel: Ekkor a feladat megoldható az alábbi szekvenciával:
Bizonyítás: Kibővítjük az állapotteret egy újabb
(
típusú) komponenssel, melynek változója legyen
. A
szekvencia közbülső feltétele legyen
|
|
Ekkor a szekvencia levezetési szabálya alapján a megoldás triviálisan teljesül.
_