- Limitation:
- $p$ $|->$ $q$ holds in $F$, $G$.
- $p$ $|->$ $q$ need
*not*hold in $F$ [] $G$!.

- Specification of program
*components*.- Given: a program component $F$.
- Wanted: properties of $F$ [] $G$ (for unknown $G$).

- Technique: conditional properties.
- Two parts (sets of unconditional properties).
- Hypothesis: specification of system ($F$ [] $G$).
- Conclusion: effect of embedding $F$ into system.
- Given hypothesis as premise.
- Conclusion can be proven from $F$ alone.

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine $$