Legyen adott tulajdonság. A feladat az, hogy keressük meg azt a legkisebb tulajdonságú egész számot, amely nem kisebb, mint az adott szám.

A feladatot ciklussal oldjuk meg. Az invariánshoz gyengítjük az utófeltételt, elhagyjuk belőle -t:

Tétel: Az alábbi struktogram formában megadott program megoldása a fent specifikált feladatnak:

Bizonyítás: A tétel a levezetési szabályokból, és a specifikáció tételéből a fentiek szerint következik. __

A fenti program csak akkor megoldása a feladatnak, ha a tulajdonság megengedett feltétel. Ha ez nem így van, akkor másik megoldást kell keresnünk. Válasszuk az alábbi invariánst (a feladat marad ugyanaz!):

Ekkor:

Tétel: Ekkor az alábbi program is megoldása a specifikált feladatnak.

Tegyük fel, hogy és létezik , hogy . Keressük meg a legelső elemet (ha van olyan), amely előtt ( -től kezdve) nem volt igaz ! Ennek a változatnak már a specifikációja is más lesz, hiszen a feladat is megváltozott.

A feladatot megoldó ciklus invariánsa:

Ekkor:

Tétel: Az alábbi struktogram formában megadott program megoldása a fent specifikált feladatnak:

A fenti feladatnak van egy speciális esete, amikor tulajdonság azt mondja ki, hogy még nem értünk el egy számot, azaz egy intervallumon kell keresni. Erre a speciális esetre adunk egy másik megoldást is.

Legyen a ciklus invariáns tulajdonsága:

Ekkor:

Tétel: Az alábbi struktogram formában megadott program megoldása a fent specifikált feladatnak: