Refinement

Protocol refinement is the act of introducing new rules that apply in more specific situations than do general rules, without invalidating these more general rules. Refinement is thus an additive process, where rules accumulate, each adding specificity in a narrower context. The opposite of refinement is generalization, in which a weaker set of rules is introduced in a broader context. In PSL, refinements are normally localized to new interfaces bearing subinterface relations to the originals. Specialized protocol declarations may be attached to (parameterized by) instances of subinterfaces. Similarly, generalizations may be attached to superinterfaces.

PSL/IDL-annotated interfaces are always refinements of those described in IDL only. When two kinds of PSL/IDL interfaces differ in protocol but not operation signatures (for example, when protocols differ across ``local'' versus ``remote'' versions of components), it may be necessary in practice to construct ``dummy'' IDL interface types just to give the two types different names [5].

Of course, not all reasonable modifications are valid refinements. For example, instances of a protocol description could differ in that one corrects an error, or removes unwanted behavior, or describes a subtly different protocol, or imposes additional constraints due to changed or overlooked requirements. Valid refinements are generally limited to the following techniques, that may also be applied in reverse in the course of generalization. These techniques reflect properties of PSL that hold for all situations A, B, C containing predicates meaningful in their scopes:

 
 A  {  true } 		  A  {  false }

{  false }   A 		 {  true }   A

 A   B,  B   C   A   C 		  A   B,  B   C   A   C

 A   B,  B   C   A   C 		  A   B,  B   C   A   C

 A   B,  B   C   A   C 		  A   B,  B   C   A   C

 
 A   B   C   A   B		 A   B   C   A   B

 B   C   A   B   A		 B   C   A   B   A

 B   A,  C   B   C   A		 C   A,  C   B   B   A

 A   C,  C   B   A   B		 A   B,  C   B   A   C

Adding Rules. New rules relating new situations, as well as new constraints, may be added so long as they do not conflict with existing ones. For example, if ReadWriteFile is defined as a subinterface of ReadFile, new rules applicable to write operations may be defined in rules for ReadWriteFile. The rules for ReadFile would also still hold for all ReadWriteFile instances.

Splicing Situations. A new situation S may be spliced among existing ordered situations A and B, so long as the original relation between A and B is maintained. Thus, A B may be extended to A S B, or to A B S, or to the separate ( A S) ( A B), and so on. Splicing allows arbitrarily complex subprotocols to be inserted between existing end-points. For example, an original version of a rule for a procedural operation might list only the request and reply. A refinement may then specify internal structure such as an interaction with a helper:

 {in(req)} enable 
    {out(reply[req]())}

 {in(req)} pair {out(h = <helper->help()>)} enable 
    {in(reply[h]())} pair {out(reply[req]())}

Note that even though the was juggled around, the original sense of the relation is maintained. If necessary, this may be checked formally. For example here, the refined rule is of the form ( A B) ( B C) ( C D). From the first two clauses we see that A C. Then applying the last clause, we obtain A D, as required by the original rule.

Subdividing Situations. A situation may be split into subsituations, so long as all ordering relations are maintained across all paths along all subsituations. For example, an initial rule for a boolean operation might only list that a reply occurs, while a refinement splits apart the conditions under which it replies true versus false:

 {in(req)} enable {out(reply(b))}

 {in(req)} && {
   case {badstuff()} enable  {out(reply(FALSE))}
   case {default}    enable  {out(reply(TRUE))} }

Strengthening Relations. The relation A B or A B may be strengthened to A B when this does not conflict with other existing rules. For example, a preliminary version of a rule may use to indicate that a particular exception may result from a certain request in a certain condition. Assuming that no other existing rules indicate otherwise, a refinement may instead use to make the stronger claim that this exception is always generated under this condition. Similarly, we could strengthen the previous example to use the operator instead of if we were sure that the listed situations represented the only ways in which the TRUE and FALSE replies could occur.

Weakening and Strengthening Situations. If relation A B holds in an original specification, a refinement may add a new rule A' B', where A A' and B' B. The reverse relation holds for . These are situational analogs of type conformance and substitutability[58], ensuring that rules applying in the original versions continue to hold even when refined. For example, consider an A B rule for a Relay r with attribute broken:

 {in(m1), !broken(r)} lead {out(m2)}

In a refined version A' B', we could have a weaker left-hand-side ( A A') and a stronger right-hand-side ( B' B), leading to a stronger rule that subsumes the original version:

 {in(m1)} lead {out(m2) by(r)}

The opposite maneuver would be either superfluous or an error: If the second rule had been the original specification, then it would have already covered the first rule. And if we had wanted to restrict the second rule to the first, the relation would not be a refinement; we would create an unrelated (on this dimension) protocol and/or interface.