Refinement of the Operator Model

This page describes formally how we refine Figure 2.5 into a more detailed model so that we can connect it later to a decision procedure. To do this, we must make explicit the output of each operator and the conditions which must be satisfied to produce it. The translation for each link on the diagram is as follows:

• Find the label, S, of the source operator of the link. Construct the type restriction , where is a new variable.

• Find the label, T, of the target operator of the link. Construct the type restriction , where is a new variable.

• Find the label of the link, which will be of the form .

• Construct the term , where each is a new variable, and the set of type restrictions on the variables.

• Merge with to give .

• The final expression is

Applying this procedure to each link in Figure 2.5 we obtain:

This definition of generalises the structure of the diagram by the use of typed variables, which is an intermediate step in defining the operators. These are described by the predicate output which has three arguments: the operator name; the data output; and the conditions which must be satisfied in order for the output to be produced. These conditions are of two kinds: inputs to the operator which are shown as links in the operator diagram; and conditions internal to the operator which will be specified in the next model. The refinement from definitions (1 to 6) to operator definitions is as follows:

1.   Rewrite to , where are the quantifiers for the link and true denotes a condition which is always true.

2. Replace each of the quantifiers, , in one of the following ways (assuming the quantifier we select at each stage is of the form ):
   1.   Replace one or more of the quantifiers, each of the form , by a condition of the form (where is a subsort of S).

   2.   Remove and instantiate X to .

   3.   Replace by an operator condition of the form . The new input I must refer to X and must appear in another stream link of the form (in other words, we must have already stipulated that an input stream exists for it). It is the designer's responsibility to ensure that this condition maintains the sort condition imposed by S.

   4.   Replace by an operator condition involving X. These conditions relate the operator's communication channels and its internal decisions. It is the designer's responsibility to ensure that each condition maintains the sort condition imposed by S.

3.   The designer can choose to further constrain the operator by adding more input or operator conditions, with the proviso that input conditions must have connections as stipulated above.

Applying this to expression 3 allows us to make the following refinement steps:

 


		  1



		  2b



		  2a



		  2c



		  3



		  2d

 

• About this document ...