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