Go backward to Hierarchical Development
Go up to Top
Go forward to Decomposition of Proofs
Refinement of Components
- By decomposition, components can be refined separately:
- Process pi
output var initially 233344;
internal var ;
input var ;
loop
< := >;
if < > then
< := >
endloop
- Correctness property:
- Compositions of refined components implements GCD.
- and and
- Decomposition of proofs not so easy:
- pi pi does not hold!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine