Legyen 
egy
az egész számokon értelmezett logikai függvény. A feladat az, hogy számoljuk meg, hány
helyen igaz 
az 
intervallumban.
|
|
|
|
|
A fenti specifikációban 
, amelyre 
és 
A
feladat megoldása analóg az összegzés tételénél leírtakkal. A ciklus invariáns
tulajdonságát itt is az utófeltétel gyengítésével kapjuk (az intervallum egy
tetszőleges kezdőszeletére írjuk fel):
|
|
A továbbiakban a ciklus levezetési szabályában szereplő feltételekhez címszószerűen felsoroljuk a levezetés során előforduló elemeket.
,
,
,
a
értékadás csökkenti a terminálófüggvény értékét,
. Itt azt kell
megvizsgálni, hogy 
-ből következik-e 
.
Vegyük észre, hogy 
esetén következik, míg 
esetén – az összegzéshez hasonlóan – meg kell növelnünk
értékét.
Ezért a 
-ből
-be jutó
program az 
elágazás lesz, ugyanis az elágazás levezetési szabályát alkalmazva:
miatt
teljesül.
A fenti meggondolások alapján nyilvánvaló az alábbi tétel:
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 fenti meggondolások (levezetés) alapján következik. __