2.3 A Semantic Space for Specifications

Figure 1 can be interpreted as arising from the scientist's view of the world, as opposed to the engineer's view [Cha97]. That is, the scientist faces this situation: ``I need to explain this artifact or phenomenon ...'' The scientist's attack is to build a mathematical model of the artifact or phenomenon in question. For software the result of this activity is denoted in Figure 1 by $\mathcal{M_{C}}$, but entirely parallel diagrams arise for other sets of physical artifacts and/or phenomena and their associated model spaces. The engineer faces a slightly different situation: ``I need some artifact or phenomenon such that ...'' The engineer's task is not so much to model something which exists and needs to be explained -- though that is certainly part of it -- but something which ought to exist. Possibly many particular implementations can satisfy the engineer's specifications.

Figure 3 illustrates how we may use this observation to view the semantics of specifications. The meaning of a specification is the set of behaviors that we wish to allow as those of conforming implementations. Indeed this directly becomes the definition of the implements relation:

$$C\ \textbf{\emph{implements}}\ S \equiv \mathcal{M_{C}}(C) \in \mathcal{M_{S}}(S)$$ (1)

Similarly, it leads directly to the definition of the extends relation:

$$S_{2}\ \textbf{\emph{extends}}\ S_{1} \equiv \mathcal{M_{S}}(S_{2}) \subseteq \mathcal{M_{S}}(S_{1})$$ (2)

  

Figure 3: $\mathcal{M_{S}} : S \rightarrow \mathcal{P(B)}$ (where $\mathcal{P(B)}$ is the powerset of $\mathcal{B}$)

Here is how this approach might pan out for a software example. Suppose operational program component C is a procedure (with possibly relational, i.e., non-deterministic behavior) and specification S is a procedure specification given by a precondition and a postcondition. We might consider a point in $\mathcal{B}$ to be a binary relation on a state space $\Sigma$ (i.e., a set of ordered pairs from $\Sigma \times \Sigma$), where $(\sigma_{1}, \sigma_{2})$is in $\mathcal{M_{C}}(C)$ iff C is permitted to start with its environment in state $\sigma_{1}$ and, when doing so, might change its environment to state $\sigma_{2}$. The precondition and postcondition from S also define a binary relation $\rho(S)$ on $\Sigma$, where the precondition says where $\rho(S)$ is defined and the postcondition defines it there. We would define $\mathcal{M_{S}}(S)$ as the set of binary relations on $\Sigma$ which are at least as defined as $\rho(S)$ and which are consistent with it where both are defined.

Notice that this framework lets us consider the meanings of specifications for systems other than programs. For example, Figure 3 and the definitions of implements and extends make sense even if $\mathcal{C}$ is the set of possible cars or TV sets (or even mere descriptions thereof), $\mathcal{B}$ is the set of possible behaviors of cars or TV sets, and $\mathcal{S}$ is the set of instruction manuals for cars or TV sets, respectively.

Our suggested semantic space for specifications might seem so simple as to be obvious or trivial. But the apparent simplicity is deceiving. In fact, we do not know of any other work that addresses the question of how to define the semantics of specifications in a domain-independent way. Even limiting the focus to software specifications, we have seen little previous work on the question of tying specifications' formal semantics to those of operational program components. Stand-alone specification languages such as Larch and $\mathcal{Z}$ have formal semantics, but in them a specification such as S above apparently would denote the single relation $\rho(S)$ -- which is in $\mathcal{B}$, not in $\mathcal{P(B)}$ as in our framework. RESOLVE semantics are based on the ACTI formal model of component-based software [Edw95], which defines semantic spaces for several kinds of software components. Among these are operational software components (``concrete instances'', tantamount to $\mathcal{C}$) and specifications (``abstract instances'', tantamount to $\mathcal{S}$) for modules exporting types and/or operations. The ACTI semantic space for abstract instances is, however, essentially structurally identical to that for concrete instances. What we propose here is different. It is a general construction where the semantic space for specifications is a higher-order space, obtained directly and mechanically from $\mathcal{B}$, which is unrelated to the internal structure of $\mathcal{B}$.