Abstract
This paper presents a method for mechanically proving the soundness of a programming logic for a distributed programming language, in support of the development of verified program verification tools. We focus on:
1.
(1) how to formalize the operational semantics of a distributed programming language;
2.
(2) how to formalize the concept of program correctness for distributed programs;
3.
(3) how to mechanically prove the soundness of a programming logic with respect to the formal semantics of the language;
4.
(4) how to use the mechanized and sound logic to develop verification tools with soundness guaranteed; and
5.
(5) how to accomplish all above in the same formalism.
Our programming logic permits the verification of single processes executing in isolation and, also, the verification of the composition of concurrently executing processes. Our method demonstrates that structuring the specification of operational semantics can ease the creation of a sound and mechanized programming logic for distributed programming languages. We believe that our method can be scaled up to larger distributed programming languages and their programming logics. The Cambridge HOL theorem proving system is used in our research.