In formal specification languages for parallel processes, such as CSP and LOTOS, algebraic laws for basic operators are provided that can be used to transform process expressions, and in particular, composition of processes can be calculated using these laws. Process composition can be used to simplify and improve the specification, and also to prove properties of the specification such as deadlock absence. We here test the practicality of process composition using CSP and suggest useful techniques, working in an example with nontrivial size and complexity. We emphasize that the size explosion of composed processes, caused by interleaving of the events of component processes, is a serious problem. Then we propose a technique, which we name two-way pipe, that can be used to reduce the size of the composed process, regarded as a program optimization at specification level.

A Sheffer function is a Boolean function such that one can produce all Boolean functions by using it as a sole basic logic element, and a typical example is the NAND operation. Here we investigate two variations of this concept, that is, Sheffer with constants" and Sheffer with constants under uniform composition". These are considered as more suitable assumptions complying with real electronic circuitry. Our new results in this paper are two explicit formulas, one for the number of n-variable functions Sheffer with constants, and the other for that of those uniformly Sheffer with constants. In particular, it is shown that almost all functions are Sheffer with constants when n is large. Some numerical values of these numbers are calculated in the range of 1n6.