Spojenie programov 2
2. p ensures q in F ? G
= p unless q in F ? G ? ? ?S: S in F ? G :: {p ??q} S {q} ?
= p unless q in F ? G ?
[? ?S: S in F :: {p ? ?q} S {q} ? ?
? ?S: S in F :: {p ? ?q} S {q} ?]
= [p unless q in F ? G ? ? ?S: S in F :: {p ? ?q} S {q} ?] ?
[p unless q in F ? G ? ? ?S: S in G :: {p ? ?q} S {q} ?]
= [p unless q in F ? p unless q in G
? ? ?S: S in F :: {p ? ?q} S {q} ?] ?
[p unless q in F ? p unless q in G
? ? ?S: S in G :: {p ? ?q} S {q} ?]
= [p ensures q in F ? p unless q in G] ?
[p ensures q in G ? p unless q in F]
Dôsledky:
1. p is stable in F ? G = (p is stable in F) ? (p is stable in G)
2. p unless q in F, p is stable in G / p unless q in F ? G
3. p is invariant in F, p is stable in G / p is invariant in F ? G
4. p ensures q in F, p is stable in G / p ensures q in F ? G
5. (lokalita) Ak nieco z nasledujúcich platí pre F, kde p je lokálne k F, tak to platí aj pre F ? G (G je lubovolné):
- p unless q, p is invariant
- p ensures q
- lokálny predikát p of F: ak pouzíva len premenné lokálne ku F, t.j. môze modifikovat len premenné, ktoré pouzíva F