ast_rt

AUTHOR

Zhi Zhang
Department of Computer and Information Sciences
Kansas State University
zhangzhi@ksu.edu

Require Export ast.
Require Export rt.

This file can be auto-generated from language_template.v by running languagegen in terminal

SPARK Subset Language with Run-Time Check Decorations

We use the Ada terminology to define the terms of this subset language, which makes it easy for Ada(SPARK) users to read it; Besides, we also indicate the reference chapter (for example, ,3.5.3) in Ada 2012 RM, and formalize the language in the same (not exactly) order as they are defined in Ada 2012 RM;

Expression + RT

Inductive expRT: Type :=
    | LiteralRT: astnum -> literal -> interior_checks -> exterior_checks -> expRT
    | NameRT: astnum -> nameRT -> expRT
    | BinOpRT: astnum -> binary_operator -> expRT -> expRT -> interior_checks -> exterior_checks -> expRT
    | UnOpRT: astnum -> unary_operator -> expRT -> interior_checks -> exterior_checks -> expRT

in IndexedComponentRT, the first astnum is the ast number for the indexed component, and the second astnum is the ast number for array represented by nameRT; in SelectedComponentRT, the first astnum is the ast number for the record field, and second astnum is the ast number for record represented by nameRT;

with nameRT: Type :=
    | IdentifierRT: astnum -> idnum -> exterior_checks -> nameRT
    | IndexedComponentRT: astnum -> nameRT -> expRT -> exterior_checks -> nameRT
    | SelectedComponentRT: astnum -> nameRT -> idnum -> exterior_checks -> nameRT .

Induction scheme for expRT and nameRT

Scheme expRT_ind := Induction for expRT Sort Prop with nameRT_ind := Induction for nameRT Sort Prop.

Statement + RT

it's used for subtype declarations:

subtype declaration, e.g. subtype MyInt is Integer range 0 .. 5;
derived type declaration, e.g. type MyInt is new Integer range 1 .. 100;
integer type declaration, e.g. type MyInt is range 1 .. 10;

Inductive rangeRT: Type := RangeRT (l: Z) (u: Z).

Type Declaration + RT

Inductive typeDeclRT: Type :=
    | SubtypeDeclRT:
        astnum -> typenum -> type -> rangeRT -> typeDeclRT
    | DerivedTypeDeclRT:
        astnum -> typenum -> type -> rangeRT -> typeDeclRT
    | IntegerTypeDeclRT:
        astnum -> typenum -> rangeRT -> typeDeclRT
    | ArrayTypeDeclRT:
        astnum -> typenum -> type -> type -> typeDeclRT
    | RecordTypeDeclRT:
        astnum -> typenum -> list (idnum * type ) -> typeDeclRT .

Record objDeclRT: Type := mkobjDeclRT{
    declaration_astnum_rt: astnum;
    object_nameRT: idnum;
    object_nominal_subtype_rt: type;
    initialization_expRT: option (expRT)
}.

Record paramSpecRT: Type := mkparamSpecRT{
    parameter_astnum_rt: astnum;
    parameter_nameRT: idnum;
    parameter_subtype_mark_rt: type;
    parameter_mode_rt: mode

}.

Declaration + RT

Procedure + RT

with procBodyDeclRT: Type :=
  mkprocBodyDeclRT
    (procedure_astnum_rt: astnum)
    (procedurNameRT: procnum)
    (procedure_parameter_profile_rt: list paramSpecRT)
    (procedure_declarative_part_rt: declRT)
    (procedure_statements_rt: stmtRT).

Program + RT

Record programRT : Type := mkprogramRT{
declsRT: declRT;
mainRT: procnum
}.

Auxiliary Functions

Section AuxiliaryFunctions_RT.

  Definition procedure_statements_rt pb :=
    match pb with
      | mkprocBodyDeclRT _ _ _ _ x => x
    end.

  Definition procedure_declarative_part_rt pb :=
    match pb with
      | mkprocBodyDeclRT _ _ _ x _ => x
    end.

  Definition procedure_parameter_profile_rt pb :=
    match pb with
      | mkprocBodyDeclRT _ _ x _ _ => x
    end.

  Definition procedur_name_rt pb :=
    match pb with
      | mkprocBodyDeclRT _ x _ _ _ => x
    end.

  Definition type_name_rt td :=
    match td with
    | SubtypeDeclRT _ tn _ _ => tn
    | DerivedTypeDeclRT _ tn _ _ => tn
    | IntegerTypeDeclRT _ tn _ => tn
    | ArrayTypeDeclRT _ tn _ _ => tn
    | RecordTypeDeclRT _ tn _ => tn
    end.

  Definition subtype_range_rt (t: typeDeclRT): option rangeRT :=
    match t with
    | SubtypeDeclRT ast_num tn t r => Some r
    | DerivedTypeDeclRT ast_num tn t r => Some r
    | IntegerTypeDeclRT ast_num tn r => Some r
    | _ => None
    end.

  Definition expression_astnum_rt e :=
    match e with
    | LiteralRT ast_num l in_checks ex_checks => ast_num
    | NameRT ast_num n => ast_num
    | BinOpRT ast_num bop e1 e2 in_checks ex_checks => ast_num
    | UnOpRT ast_num uop e in_checks ex_checks => ast_num
    end.

  Definition name_astnum_rt n :=
    match n with
    | IdentifierRT ast_num x ex_checks => ast_num
    | IndexedComponentRT ast_num x e ex_checks => ast_num
    | SelectedComponentRT ast_num x f ex_checks => ast_num
    end.

End AuxiliaryFunctions_RT.