State Visibility and Communication in Unifying Theories of Programming

We explore the interactions between programvariable 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 waitperiods 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.

• Type: Conference
• Year: 2009
• Where: TASE
• Authors: Andrew Butterfield, Pawel Gancarski, Jim Woodcock
• Keywords: Cleaner Operational Intuitions, Programvariable State Visibility, Software Engineering, State-rich Csp-like Processes, TASE 2009