Go backward to The General Theorem
Go up to Top
Go forward to The Composition Theorem

Composing Assumption/Guarantee Specifications

General form:
- Assertion that system guarantees $M$ under assumption that environment satisfies $E$ .
- $E$ -|>+ $M$ .
- If environment satisfies $E$ till time $n$ , then system must satisfy $M$ till time $n+1$ .
Composition:
- Write environment assumptions are safety properties.
- Write systems's fairness guarantee as conjunction of properties $E$ _L $=>$ WF_v(A) and $E$ _L $=>$ SF_v(A) where $E$ _L is an environment fairness assumption.
- By Proposition 1, resulting specification is machine-closed (if $(P,L)$ is machine-closed and $L$ $=>$ $R$ , then $(P,R)$ is machine-closed).

Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine