25.2. Példa.
.
.
.
,
,
,
,
,
.
A . példában megadott feladat specifikációs feltételének elágazó idejű temporális
logikai megfelelője: 
, ami nem azonos a lineáris logikában is megfogalmazható
-val
(. fejezet). A specifikációs eszközök kifejezőereje tehát meghaladja a
UNITY kifejezőerejét.
A szekvenciális programoktól eltérően a most definiált absztrakt program helyességének igazolásához megfogalmazott programtulajdonságok nem külön-külön az egyes utasításokra, hanem a teljes utasításhalmazra vonatkoznak. Ez úgy is megfogalmazható, hogy a bizonyítás és a programszöveg szétválik. Azt is mondhatjuk, hogy a módszer a globális invariánsok módszerének általánosítása [[???And 91]]. (Megj.: A bizonyítás és a programszöveg szétválasztása lehetséges szekvenciális programok esetén is, lásd: [[???Lam 90]]).