Go backward to Refinement of Components
Go up to Top
Go forward to Composing Open Systems

Decomposition of Proofs

pi_a^l does not implement pi_a
- No assumptions when $b$ can change.
- pi_a^l can behave in ways that pi_a cannot!
- pi_a can increment $a$ only by current value of $b$ .
- pi_a^l can increment $a$ by previous value of $b$ (if $b$ changes after assignment to $ai$ )
Context assumption:
- $E$ _a $<=>$ $b$ does not change when $a>b$ .
- $E$ _a and $M$ _a^l $=>$ $M$ _a.
Basic proof idea (not yet fully correct)
- $E$ _a and $M$ _a^l $=>$ $M$ _a
  $E$ _b and $M$ _b^l $=>$ $M$ _b
  $M$ _a and $M$ _b $=>$ $E$ _a and $E$ _b
Decomposition leads simpler proofs:
- $E$ _a significantly simpler than $M$ _b^l.
- $M$ _a and $M$ _b $=>$ $E$ _a and $E$ _b simpler than direct proof of specification.

Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine