Report Number: CSL-TR-86-301
Institution: Stanford University, Computer Systems Laboratory
Title: The complete transformation methodology for sequential runtime
Author: Sankar, Sriram
Author: Rosenblum, David
Date: June 1986
Abstract: We present in this report a complete description of a methodology for transformation of Anna (Annotated Ada) programs to executable self-checking Ada programs. The methodology covers a subset of Anna which allows annotation of scalar types and objects. The allowed annotations include subtype annotations, subprogram annotations, result annotations, object annotations, out annotations and statement annotations. Except for package state expressions and quantified expressions, the full expression language of Anna is allowed in the subset. The transformation of annotations to executable checking functions is thoroughly illustrated through informal textual description, universal checking function templates and several transformation examples. We also describe the transformer and related software tools used to transform Anna programs. In conclusion, we describe validation of the transformer and some methods of making the transformation and runtime checking processes more efficient.
http://i.stanford.edu/pub/cstr/reports/csl/tr/86/301/CSL-TR-86-301.pdf