Legyen egy tetszőleges halmaz, egy egész szám, továbbá függvény, rögzített, és definiáljuk az függvényt az alábbi módon:

továbbá :

Feladatunk az, hogy meghatározzuk az függvény helyen felvett értékét.

Tétel: Az alábbi struktogrammal adott program megoldása a specifikált feladatnak:

Bizonyítás: 

A tétel bizonyításához elegendő, ha a fenti programot levezetjük, hiszen ekkor az állítás a specifikáció tételéből és a levezetési szabályokból következik. Legyen tehát a megoldóprogram egy ciklus, melynek invariánsa:

Vizsgáljuk meg a ciklus levezetési szabályának feltételrendszerét:

_

Megjegyezzük még, hogy a 0 kezdőpont választása önkényes, bármilyen tetszőleges egész számtól kezdve definiálható egy függvény, és akkor értelemszerűen a program ciklusváltozója is arról az értékről indítandó.