Systematically Constructing a CCS Interpreter - Summary

Correctness is a major concern in computer science, especially for programs with complicated semantics that people have to depend on, such as compilers and interpreters. One of the new paradigms of computer science is that it is better to ensure correctness by construction and transformation than by a posteriori proof. Most examples of the application of this paradigm, however, have been small. In this paper a transformational approach to the construction of an efficient `interpreter' for a specification language is described. One of its applications has been LOTOS, a language for specifying communication protocols. Because of space constraints however, we will discuss here the application to CCS, a smaller language, which inspired LOTOS