No. 383 (1992): PB-383 An Automatically Generated and Provably Correct Compiler for a Subset of Ada