Components

Our laws can be used to reason, based on syntactic conditions, whether two specifications are equivalent.

• Specification Matching of Software Components
  

Zaremski and Wing determines whether two software components are related by a specification matching process. This can be useful, among other things, to reuse components and substitute one component by another without affecting the observable behaviour. To verify whether the specification of one component matches the other, the authors use a theorem prover. We believe that our set of laws can be useful in this case. Suppose that each Java component is annotated with Alloy. Since we already proved that our laws are semantics-preserving, applying the laws, we just have to check syntactically whether one specification component is equivalent to another, instead of proving it. However, since we do not prove that our set of laws is complete, we may not use them always.

<< Back