Legyen
egy olyan halmaz, amin értelmezve van egy rendezési reláció. Legyen
monoton növekedő függvény. A feladat az, hogy döntsük el az
függvényről, hogy
az adott
intervallumon
felveszi-e a
adott
értéket, és ha igen, akkor adjuk meg az intervallum egy olyan pontját, ahol a függvényérték
.
|
|
|
|
|
|
|
A monotonitást felhasználva az intervallumot mindkét végéről szűkítjük az invariánsban:
|
|
|
|
Ekkor
,
,
Informálisan fogalmazva jelölje a még megvizsgálandó elemek számát. Ezt egy esetszétválasztással
adhatjuk meg:
A ciklusmag legyen egy szekvencia, melynek közbülső feltétele:
|
|
|
|
Ekkor a szekvencia első fele lehetne az
értékkiválasztás. Hatékonysági szempotokat is figyelembe
véve azonban válasszuk az intervallum középső elemét:
. A ciklusmag második felében három eset lehetséges:
: ekkor az
értékadás az invariánst megtartja,
: ekkor megtaláltuk a keresett elemet, tehát
,
: ekkor az
értékadás az invariánst megtartja.
Egyszerűen ellenőrizhető, hogy a fenti elágazás mindhárom ága csökkenti a termináló függvényt.
Tétel: Az alábbi struktogram formában megadott program megoldása a fent specifikált feladatnak:
Bizonyítás: A tétel a fenti levezetés következménye.