A HOL MECHANIZATION OF THE AXIOMATIC SEMANTICS OF A SIMPLE DISTRIBUTED-PROGRAMMING LANGUAGE

This paper presents the axiomatic semantics for a simple distributed language, and its mechanization in HOL. The constructs of this language include those basic to a very simple sequential programming language in addition to asynchronous send and synchronous receive statements. The language has the appearance of a system programming language that supports sequential execution extended with message passing, and would be a suitable basis for coding distributed operating systems and applications. Included in the mechanization are functions which generate the goals associated with the verification of sequences of simple statements in the language. In contrast to Gordon's work on the HOL mechanization of programming logics, the starting point for our work is an axiomatic (rather than denotational definition) of the language, in the style of Schlichting's definition of message passing.