A Hierarchical Method for Reasoning about Distributed Programming Languages

. This paper presents a technique for specifying and reasoning about the operational semantics of distributed programming languages. We formalize the concept of "vertical stacking" of distributed systems, an extension of Joyce's, Windley's and Curzon's stacking methodologies for sequential systems and of the CLI "short stack" which stacks interpreters for object code, assembly code, and a high-level sequential language. We use a state transition model to account for the issues of atomicity, concurrency and nondeterminism at all levels in our stack. A correctness definition is given, which for each pair of adjacent language semantics and mappings between them, produces proof obligations corresponding to the correctness of the language implementation. We present an application of the method to a two-level stack: the microSR distributed programming language and a multi-processor instruction set, which is the target language for a compiler for microSR. We also present the development of a ..