Spojenie programov
nech F, G sú dva UNITY-programy
spojenie programov F a G, oznacenie F ? G
- spoja sa zodpovedajúce si casti z F a G
- predpokladá sa, ze nevznikajú nekonzistentcie s premennými, inicializáciou, always sekciou apod.
Spojovacia veta:
1. p unless q in F ? G =
p unless q in F ? p unless q in G
2. p ensures q in F ? G =
[p ensures q in F ? p unless q in G] ?
[p ensures q in G ? p unless q in F]
3. (FP of F ? G) = (FP of F) ? (FP of G)
Dôkaz:
3. priamo z definície
1. p unless q in F ? G
= ? ?S: S in F ? G :: {p ? ?q} S {p ? q} ?
= ? ?S: S in F :: {p ? ?q} S {p ? q} ? ?
? ?S: S in G :: {p ? ?q} S {p ? q} ?
= p unless q in F ? p unless q in G