Constructing Theories about Specifications
Given a specification we can prove many things about it, constructing a theory of that specification, increasing our understanding and reinforcing our faith in its correctness.
The classroom specification:
- If someone leaves the classroom and re-enters it, the state of the classroom should be unaltered.
- (Leave1; Enter1) ? (? Class1 | p? ? d)
? Class1 | p? ? d
? <by definition>
(#d <= Max ? #d’ <= Max ? d’ = d ? p? ? d)