Špeciálne prípady unless (stable, invariant)
p is stable ? p unless false
q is invariant ? (initial condition ? q) ? q is stable
ak p is stable, tak ak sa teraz stane true, potom ostane vzdy true (? {p} S {p} pre ?S)
Pozorovanie: Ak I, J sú stable (pre program F), potom aj I ? J, I ? J sú stable. Podobne pre invarianty.
Oznacenie: constant p: ak p aj ?p sú stable
Substitucná axióma: Ak x = y je invariant programu F, tak môzeme x zamenit za y vo všetkých vlastnostiach programu F.
Ak I je invariant, je zamenitelný s true a vice versa.
Dôsledok: p unless q, ?q is invariant ? p is stable.
Dôkaz:
?q ? true /* substitucná axióma */
p unless q /* predpoklad */
p unless false /* z predchádzajúcich */
p is stable /* z definície */
Ak I je invariant, tak p môze byt zamenitelné s I ? p alebo ?I ? p a podobne.
Dokázat, ze p je stabilné: stací ukázat, ze I ? p je stabilné, co môze byt lahšie, ako pre samotné p.