A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler

An interpreter for an imperative programming language called Minila has been formally specified in CafeOBJ, an executable specification language, and so have a virtually machine (VM) and a compiler. The compiler transforms a Minila program into an instruction sequence processed by the VM. Since the formal specifications are executable, it is doable to test if for any concrete terminating program p the result of interpreting p is the same as the one of processing by the VM the instruction sequence generated from p by the compiler, where the result is an environment, a variable-value pair collection. The equivalence is called the Minila compiler correctness with respect to p. In addition to test, properties of CafeOBJ specifications can be theorem proved by writing what are called proof scores in CafeOBJ and executing them with CafeOBJ. The Minila compiler correctness for all terminating programs in Minila has been theorem proved.