Go backward to Collaries
Go up to Top
Go forward to Example
Specifications that Compose
- Limitation:
- holds in , .
- need not hold in [] !.
- Specification of program components.
- Given: a program component .
- Wanted: properties of [] (for unknown ).
- Technique: conditional properties.
- Two parts (sets of unconditional properties).
- Hypothesis: specification of system ( [] ).
- Conclusion: effect of embedding into system.
- Given hypothesis as premise.
- Conclusion can be proven from alone.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine