Theories of translation correctness for concurrent programming languages

Abstract

This thesis addresses the problems of defining and proving translation correctness for programming languages describing concurrent processes. Taking an operationally motivated approach two distinct theories are proposed, a bisimulation theory and a testing theory, and both are articulated on substantial examples.

The bisimulation approach is applied to an example translation from a variant of CSP to CCS by defining a syntax-directed context-sensitive translation from CSP to CCS and establishing the correctness criteria of the bisimulation approach.

The testing approach provides two possible correctness criteria; implementation and complete-implementation, of which the latter implies the former. A substantial example of each is given. In demonstrating complete-implementation the example translates handshake communication in a CSP-like language to shared variable communication in an artificial language manipulating a communication state. For implementation we consider the design and specification of a concurrent sorting machine in CCS for which the design does not completely implement the specification.