Go backward to Refinement of Components
Go up to Top
Go forward to Composing Open Systems
Decomposition of Proofs
- pi does not implement pi
- No assumptions when can change.
- pi can behave in ways that pi cannot!
- pi can increment only by current value of .
- pi can increment by previous value of (if changes
after assignment to )
- Context assumption:
- does not change when .
- and .
- Basic proof idea (not yet fully correct)
- Decomposition leads simpler proofs:
- significantly simpler than .
- and and simpler than direct
proof of specification.
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine