CpdtTactics

list_util

• List Split Operations
• List Split Lemmas

ast_basics

• Identifiers
• Data Types
• In/Out Mode
• Operators
• Literals
• Auxiliary Functions

ast

• SPARK Subset Language
  • Expression
  • Statement
  • Type Declaration
  • Declaration
  • Procedure
• Program
• Auxiliary Functions

ast_rt

• SPARK Subset Language with Run-Time Check Decorations
  • Expression + RT
  • Statement + RT
  • Type Declaration + RT
  • Declaration + RT
  • Procedure + RT
  • Program + RT
• Auxiliary Functions

ast_util

• Auxiliary Functions for AST
• Auxiliary Functions for AST_RT

rt

• Run-Time Checks
• Run-Time Checks Subset

values

• Run-Time Error
• Return Value / State
• Value
• Bound of Value
• Value Operation
  • Arithmetic Operation
  • Logic Operation
  • Relational Operation
• Binary Operation
• Unary Operation

environment

• Store
  • Store Operation
  • Lemmas About Store Operation
• State
  • State Operation
  • Lemmas About State Operation

symboltable_module

• Symbol Table Element
• Symbol Table Module
  • Symbol Table Structure
  • Name Table Operation
  • Symbol Table Operation

symboltable

• Symbol Table
  • SymTab
  • SymTabRT
• Symbol Table Operation
  • Symbol Table Operation for AST
  • Symbol Table Operation for AST_RT
• Help Lemmas

eval

• Run-Time Check Evaluation
  • Overflow Check
  • Division Check
  • Range Check
  • Run-Time Check for Binary Operator
  • Run-Time Check for Unary Operator
• Relational Semantics
  • Literal Evaluation
  • Expression Evaluation
  • Name Evaluation
  • Declaration Evaluation
  • Statement Evaluation
    • Copy In
    • Copy Out
  • evalStmt
  • evalProgram

eval_rt

• Run-Time Check Evaluation + RT
  • Run-Time Check for Binary Operator + RT
  • Run-Time Check for Unary Operator + RT
• Relational Semantics
  • Evaluation of Literal + RT
  • Evaluation of Expression + RT
  • Evaluation of Name + RT
  • Evaluation of Declaration + RT
  • Evaluation of Statement + RT
    • Copy In + RT
    • Copy Out + RT
    • evalStmtRT
  • evalProgramRT
• Help Lemmas

rt_gen

• toExpRT
• toNameRT
• toArgsRT
• toStmtRT
• toDeclRT
• toProcBodyDeclRT
• toProgramRT

rt_gen_impl

• toExpRTImpl
• toNameRTImpl
• toArgsRTImpl
• toStmtRTImpl
• toDeclRTImpl
• toProcBodyDeclRTImpl
• toProgramRTImpl

rt_gen_impl_consistent

• Semantics Consistency Proof for Run-Time Check Generator
• Soundness of RT-GEN Implementation
  • toExpRTImpl_soundness
  • toNameRTImpl_soundness
  • toArgsRTImpl_soundness
  • toStmtRTImpl_soundness
  • toDeclRTImpl_soundness
  • toProcBodyDeclRTImpl_soundness
  • toProgramRTImpl_soundness
• Completeness of RT-GEN Implementation
  • toExpRTImpl_completeness
  • toNameRTImpl_completeness
  • toArgsRTImpl_completeness
  • toStmtRTImpl_completeness
  • toDeclRTImpl_completeness
  • toProcBodyDeclRTImpl_completeness
  • toProgramRTImpl_completeness
• Consistency of RT-GEN Impl and RT-GEN Spec
  • toExpRTImplConsistent
  • toStmtRTImplConsistent
  • toProcBodyDeclRTConsistent
  • toProgramRTImplConsistent

rt_gen_consistent

• Helper Lemmas
• Soundness of RT-GEN Specification
  • toExpRT_soundness
  • toNameRT_soundness
  • toDeclRT_soundness
  • storeUpdateRT_soundness
  • copyInRT_soundness
  • copyOutRT_soundness
  • toAssignStmtRT_soundness
  • toStmtRT_soundness
  • toProgramRT_soundness
• Completeness of RT-GEN Specification
  • toExpRT_completeness
  • toNameRT_completeness
  • toDeclRT_completeness
  • storeUpdateRT_completeness
  • copyInRT_completeness
  • copyOutRT_completeness
  • toAssignStmtRT_completeness
  • toStmtRT_completeness
  • toProgramRT_completeness
• Consistency of RT-GEN Spec
  • toExpRTConsistent
  • toNameRTConsistent
  • toDeclRTConsistent
  • toStmtRTConsistent
  • toProgramRTConsistent

rt_gen_util

• Helper Lemmas for RT-GEN
• SymTabRT Generator
  • Help Lemmas for SymTabRT

rt_opt_ZArith

• ZArith (Mult, Div, Mod)
  • Mult
  • Div
  • Mod
• Relation (Zeq, Zlt, Zle, Zgt, Zge)
  • Relation between Zlt and Zlt_bool
  • Zlt_bool
  • Zlt
• ZArith Lemma
  • Min Lemmas
  • Max Lemmas
  • Zmult Lemmas
  • Zquot Lemmas
• Modulus Interval Correctness
• Multiply Interval Correctness
• Divide Interval Correctness

rt_opt

• Run-Time Checks Optimization Rule
  • optimize_overflow_check
  • optimize_range_check
  • optimize_range_check_on_copy_out
  • optimize_rtc_binop
  • optimize_rtc_unop
• Run-Time Checks Optimization
  • Checks Optimization for Literal
  • Checks Optimization for Expression
  • Checks Optimization for Name
  • Checks Optimization for Arguments
  • Checks Optimization for Statement
  • Checks Optimization for Declaration
  • Checks Optimization for Procedure
  • Checks Optimization for Program

rt_opt_impl

• executable check optimization functions
• Run-Time Checks Optimization
  • Checks Optimization for Expression
  • Checks Optimization for Name
  • Checks Optimization for Arguments
  • Checks Optimization for Statement
  • Checks Optimization for Declaration
  • Checks Optimization for Procedure
  • Checks Optimization for Program

rt_opt_impl_consistent

• helper lemmas
  • extract_subtype_range_f soundness and completeness
  • bound_of_type_f soundness and completeness
  • bound_of_array_component_type_f soundness and completeness
  • bound_of_record_field_type_f soundness and completeness
  • in_bound_f soundness and completeness
  • sub_bound_f soundness and completeness
  • optimize_overflow_check_f soundness and completeness
  • optimize_range_check_f soundness and completeness
  • optimize_range_check_on_copy_out_f soundness and completeness
  • optimize_rtc_binop_f soundness and completeness
  • optimize_rtc_unop_f soundness and completeness
  • extract_array_index_range_f soundness and completeness
• Consistency Proof for RT-OPT Implementation
• Soundness of RT-OPT Implementation
  • optLiteralImpl_soundness
  • optExpImpl_soundness
  • optNameImpl_soundness
  • optArgsImpl_soundness
  • optStmtImpl_soundness
  • optObjDeclImpl_soundness
  • optDeclImpl_soundness
  • optProgramImpl_soundness
• Completeness of RT-OPT Implementation
  • optLiteralImpl_completeness
  • optExpImpl_completeness
  • optNameImpl_completeness
  • optArgsImpl_completeness
  • optStmtImpl_completeness
  • optObjDeclImpl_completeness
  • optDeclImpl_completeness
  • optProgramImpl_completeness
• Consistency of RT-OPT Impl and RT-OPT Spec
  • optExpImplConsistent
  • optNameImplConsistent
  • optStmtImplConsistent
  • optDeclImplConsistent
  • optProgramImplConsistent

rt_opt_util

• Helper Lemmas for RT-OPT
  • in_bound Lemmas
  • run-time erasion Lemmas
  • RT-OPT exterior checks Lemmas
  • Other Lemmas

well_typed

• Helper Functions
  • type of the expression
• Well-Typed Expression
• Well-Typed Statement
• Well-Typed Declaration
• Well-Typed Program
• well typed symbol table
• Well-Typed Value
• Well-Typed Store
• Well-Typed State
• Well-Typed State and Symbol Table

well_typed_util

• Helper Lemmas
• well-typed store and stack lemmas
• storeUpdate_preserve_typed_stack
• Eval Exp_or_Name Value Well Typed
• Typed Value in Bound
• copy_in_preserve_typed_store
• copy_out_preserve_typed_stack
• eval_declaration_preserve_typed_stack
• cut_until_preserve_typed_stack
• eval_statement_preserve_typed_stack
• wellTypedStatePreservation

rt_opt_consistent_util

• Eval Expr Value In Bound
• Eval Name Value In Bound
• Soundness of RT-OPT Specification
  • Helper Lemmas
  • optExp_soundness
  • optName_soundness
  • storeUpdateRT_opt_soundness
  • optArgs_copyin_soundness
• Completeness of RT-OPT Specification
  • optExp_completeness
  • optName_completeness
  • storeUpdateRT_opt_completeness
  • optArgs_copyin_completeness
• help version with well_typed_value_in_stack and well_typed_value_in_store

rt_opt_consistent

• Soundness of RT-OPT Specification
  • optArgs_copyout_soundness
  • optStmt_soundness
  • optDecl_soundness
  • optProgram_soundness
• Completeness of RT-OPT Specification
  • optArgs_copyout_completeness
  • optStmt_completeness
  • optDecl_completeness
  • optProgram_completeness
• Consistency of RT-OPT Spec
  • optExpConsistent
  • optStmtConsistent
  • optDeclConsistent
  • optProgramConsistent

rt_counter

• Count Number of Run-Time Checks
  • Check Counter for Expression
  • Check Counter for Name
  • Check Counter for Statement
  • Check Counter for Declaration
  • Check Counter for Procedure

rt_validator

• Run-Time Check Validator
  • Run-Time Check Validator for Expression
  • Run-Time Check Validator for Name
  • Run-Time Check Validator for Statement
  • Run-Time Check Validator for Declaration
  • Run-Time Check Validator for Procedure
  • Run-Time Check Validator for Program
• Map Back to SPARK Source Code