2.1 Problem Being Addressed

The purpose of defining a formal semantics for a language is to give precise meanings to the strings in that language. In principle, it is relatively well understood how to define the semantics of operational program components in a programming language such as C or Pascal. Of course as a practical matter, defining the formal semantics for most programming languages is an enormous chore, but this is unimportant for the current paper. What we seek is simply a framework in which such a semantics might be defined, as illustrated in Figure 1. For each string which is an operational program component in the language (i.e., an element of $\mathcal{C}$), the semantic function $\mathcal{M_{C}}$ assigns to it a run-time behavior (i.e., an element of $\mathcal{B}$). In this paper we constrain neither the structure of $\mathcal{B}$ nor the semantic function $\mathcal{M_{C}}$, except to stipulate that $\mathcal{M_{C}}$ is total.

  

Figure 1: $\mathcal{M_{C} : C \rightarrow B}$

Now consider a combined specification-and-implementation language such as RESOLVE, or a hybrid that combines a specification language (e.g., Larch or RESOLVE or $\mathcal{Z}$) with a modern implementation programming language with templates (e.g., Ada or C++ or RESOLVE). As shown in Figure 2, such a language also contains strings which are specifications and templates. As noted above, the meanings of these strings might not be elements of $\mathcal{B}$. What do specifications and templates mean? And more important, how are these meanings connected to those of operational program components?

  

Figure 2: $\mathcal{M_{S} : S \rightarrow ???}$ and $\mathcal{M_{T} : T \rightarrow ???}$