State Visibility and Communication in Unifying Theories of Programming

We explore the interactions between program-variable state visibility and communication behaviour in state-rich CSP-like processes, using the Unifying Theories of Programming (UTP) framework. The key results of this work are: having variable state visible while a process is waiting to communicate, results in an operationally complex theory of behaviour; by contrast, considering state as unobservable during communication wait periods results in an elegant theory, with much cleaner operational intuitions. The language constructs most affected by this observability choice are those of external choice and parallel composition. We also discuss situations where this state hiding can prevent the adoption of interesting operators that seize control from waiting processes.