Első példánk csatornaváltozók használatára a ábrán látható természetes számokat generáló folyamat specifikációja és az azt megvalósító program. A -gyel jelölt folyamat a folyamathálózat egy eleme, az általa generált számokat más folyamat(ok) használják fel.

A folyamat állapot- és paraméterterében egy egész típusú csatornaváltozó és ugyanezen csatorna történetváltozója jelenik meg. Mindkét változó értéke kezdetben az üres sorozat a kikötés szerint.

Az csatorna történetváltozója segítségével könnyen megfogalmazhatjuk, hogy a csatornán egymás után, növekvő sorrendben a természetes számok jelennek meg (): invariáns, hogy a csatorna történetének értéke a természetes számok sorozatának kezdő részsorzata. A csatornaváltozó segítségével nagyon nehéz lenne előírni hasonló követelményt. A csatornaváltozó értéke bármikor lehet az üres sorozat, így semmilyen támpontot sem ad arra nézve, hogy melyik volt az előző érték, amelyik megjelent rajta. Az invariánst a legkönnyebben úgy teljesíthetnénk, ha soha egyetlen elemet sem helyeznénk az csatornára, az üres sorozat mindig prefixe a természetes számok sorozatának. A kikötés azonban megköveteli, hogy az csatorna történetének hossza elkerülhetetlenül növekedjen. Figyeljük meg, hogy a feladat nem fogalmaz meg sem terminálási, sem fixpont feltételt. Terminálás helyett végtelen működést követel meg.

A megoldás megtalálása érdekében bővítjük az állapotteret és finomítjuk a specifikációt:

Könnyen beláthatjuk a levezetési szabályok segítségével (. fejezet), hogy a új specifikáció szigorúbb az előzőnél (.) és (.)-ből következik (.), ill. (.)-ból következik (.).

A megoldó program a következő:

Bizonyítás: Megmutatjuk, hogy a program megfelel a finomított specifikációnak.

(): Megmutatjuk, hogy

.

():

():

és

.