The CCS model of interprocess communication lends itself to the specification of module interfaces in terms of structures of messages. When a weakly determinate module q is specified and is broken into two submodules, one of which, p, is specified, the goal is to derive the specification of the other submodule, r; that is, (p|r)\A=q is to be solved for r, where A is the vocabulary of p that is not in q, | is parallel composition, \ is a message hiding operation, and = is observational equivalence. Shields gives a constructive proof for r together with the conditions necessary for a solution to exist.

The paper consists largely of definitions of the mathematical machinery used in constructing the solution; indeed, its overall purpose is to demonstrate the value of the math in the analysis of specifications using sets of possible future messages (as related to trace semantics). The choice of CCS means that concern with the silent message &tgr; lengthens the proofs. An alternative approach would be to view communication structures as directed graphs; the problem then becomes one of graph unification, such that any message of q that is not in p must be in r, and any message of p that is not in q must have its dual in r. Shields does not address the question of relations between the values carried by messages. The restriction of q to weak determinacy is reasonable, but consideration of the more general case would be worthwhile. The essential problem of how q should be partitioned into p and r in the first place is not, and perhaps cannot be, resolved. Despite these problems, the approach seems viable and is worth looking at for those with an interest in CCS and specification structures.