BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CSL-TR-86-301
       ENTRY:: November 08, 1994
ORGANIZATION:: Stanford University, Computer Systems Laboratory
       TITLE:: THE COMPLETE TRANSFORMATION METHODOLOGY FOR SEQUENTIAL
               RUNTIME CHECKING OF AN ANNA SUBSET
        TYPE:: Technical Report
      AUTHOR:: Sankar, Sriram
      AUTHOR:: Rosenblum, David
        DATE:: June 1986
       PAGES:: 64
    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.
       NOTES:: [Adminitrivia V1/Prg/19941108]
         END:: STAN//CSL-TR-86-301