Parallel Composition

A complex specification will typically be constructed as a colimit of simpler component specifications. To build a refinement of such a specification, we will most likely first build refinements on its components. The refinement of the complex specification will then be obtained by a parallel composition of these component refinements. This composition is performed by the same colimit operation, applied to refinements, that we have already applied to specifications.

The Specware implementation will ensure that the component refinements are compatible; if they employ inconsistent representations for entities that are shared between components, a parallel composition may not exist. For instance, in refining the plane geometry theory, we couldn't form a parallel composition of two refinements of rectangles and rhombuses, respectively, if one represented a line segment as a pair of pairs (each corresponding to an endpoint) and the other as a triple of a pair and two reals (corresponding to an endpoint, a slope, and a length). This is not to say that we cannot employ multiple representations of a line segment, just that we cannot use parallel refinement for that purpose.