A verified code generator for a subset of gypsy

Abstract

This report describes the specification and mechanical proof of a code generator for a subset of Gypsy 2.05 called Micro-Gypsy. Micro-Gypsy is a high-level language containing many of the Gypsy control structures, simple data types and arrays, and predefined and user-defined procedure definitions including recursive procedure definitions. The language is formally specified by a recognizer and interpreter written as functions in the Boyer-Moore logic. The target language for the Micro-Gypsy code generator is the Piton high-level assembly language verified by J Moore to be correctly implemented on the FM8502 hardware. The semantics of Piton is specified by another interpreter written in the logic. A Boyer-Moore function maps a Micro-Gypsy state containing program and data structures into an initial Piton state. We prove that an arbitrary legal Micro-Gypsy program is correctly implemented in Piton. By this we mean that execution of the resulting Piton state is semantically equivalent (under a mapping function we exhibit) to the result of executing the initial Micro-Gypsy state with the Micro-Gypsy interpreter. An interesting fact of our implementation is that we pass procedure parameters efficiently by reference even though we use a value-result semantic definition. We are not aware of any previous mechanical proof that passing parameters by reference correctly implements value-result semantics. In this report we define Micro-Gypsy and Piton, describe the translation process, and explain the correctness theorem proved.