A verified code generator for a subset of gypsy

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