Theories of Translation Corrections for Concurrent Programming Languages

M. Millington

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.

Ph.D. Thesis - Price £8.00

LFCS report ECS-LFCS-87-39

Previous | Index | Next