A formal proof of correctness of construct association from PROMELA to Java

subset of Java's constructs is intended to provide a collection of rules that can be used as a reference in developing a model of code translator from a PROMELA model to a Java program. The idea arises from the fact that, both PROMELA model and Java program are built (or composed) by various elementary elements called constructs. Although this kind of association has already been introduced in some previous researches, they provided no proofs about its correctness. In this paper we propose a formal proof of association's correctness by showing the equivalence (or similarity) of the program graphs for every two associated constructs in the association. The correctness of association means that every two associated constructs in association have equivalent semantics. In addition, at the end of this paper we also introduce a translator tool we have developed based on this association's definition to translate PROMELA model to Java program.