Extensibella Example: exactEval:assert

Language Specification

File: defs.sos

[Reduce File] [Raw File] 
Module exactEval:assert

Builds on exactEval:host

stmt ::= ...
       | assert(expr, expr)


-------------------------------------------- [Proj-Assert]
Names |{stmt}- assert(E, Msg) ~~>
         ifThenElse(E, noop,
            /*printVal(error) never succeeds*/
            printVal(errorExpr(Msg, intTy)))



typeOf FC TC E boolTy
typeOf FC TC Msg stringTy
------------------------------ [T-Assert]
stmtOK FC TC assert(E, Msg) TC



exprNames Ctx E NE
exprNames Ctx Msg NM
NE ++ NM = N
---------------------------------- [SN-Assert]
stmtNames Ctx assert(E, Msg) N Ctx



evalExpr FE EE E trueVal EE2 O
----------------------------------- [E-Assert]
evalStmt FE EE assert(E, Msg) EE2 O

Reasoning

[Show All Proofs] [Hide All Proofs] [Raw File]

Click on a command or tactic to see a detailed view of its use.

Module exactEval:assert.

/********************************************************************
 Basic Projection Constraints
 ********************************************************************/
Prove_Constraint exactEval:host:proj_expr_unique.
Prove_Constraint exactEval:host:proj_expr_is.
Prove_Constraint exactEval:host:proj_expr_other.

Prove_Constraint exactEval:host:proj_stmt_unique. [Show Proof]

Prove_Constraint exactEval:host:proj_stmt_is. [Show Proof]

Prove_Constraint exactEval:host:proj_stmt_other. [Show Proof]


Prove_Constraint exactEval:host:proj_fun_unique.
Prove_Constraint exactEval:host:proj_fun_is.

Prove_Constraint exactEval:host:proj_param_unique.
Prove_Constraint exactEval:host:proj_param_is.

Prove_Constraint exactEval:host:proj_program_unique.
Prove_Constraint exactEval:host:proj_program_is.

Prove_Constraint exactEval:host:proj_typ_unique.
Prove_Constraint exactEval:host:proj_typ_is.




/********************************************************************
 Decidable Equality
 ********************************************************************/
Add_Proj_Rel exactEval:host:is_expr, exactEval:host:is_args,
             exactEval:host:is_recFieldExprs, exactEval:host:is_stmt.
Prove_Ext_Ind exactEval:host:is_expr, exactEval:host:is_args,
              exactEval:host:is_recFieldExprs, exactEval:host:is_stmt. [Show Proof]


Prove exactEval:host:is_args_nilArgs_or_consArgs.
Prove exactEval:host:is_recFieldExprs_nilRecFieldExprs_or_consRecFieldExprs.




/********************************************************************
 Variables
 ********************************************************************/
Prove exactEval:host:vars_unique.

Prove exactEval:host:vars_is.

Prove exactEval:host:vars_exist,
      exactEval:host:varsArgs_exist,
      exactEval:host:varsRecFields_exist.




/********************************************************************
 Statement Names
 ********************************************************************/
Prove exactEval:host:stmtNames_is,
      exactEval:host:stmtNames_isCtx,
      exactEval:host:exprNames_is. [Show Proof]


Prove exactEval:host:stmtNames_unique,
      exactEval:host:exprNames_unique. [Show Proof]


Prove exactEval:host:stmtNames_keep_older. [Show Proof]


Prove exactEval:host:stmtNames_exists,
      exactEval:host:exprNames_exists,
      exactEval:host:argsNames_exists,
      exactEval:host:recFieldNames_exists. [Show Proof]


Prove exactEval:host:stmtNames_not_in_ctx,
      exactEval:host:exprNames_not_in_ctx. [Show Proof]



Prove exactEval:host:stmtNames_relatedCtxs,
      exactEval:host:stmtNames_relatedCtxs_ctx_fwd,
      exactEval:host:stmtNames_relatedCtxs_ctx_back,
      exactEval:host:exprNames_relatedCtxs. [Show Proof]



Prove exactEval:host:stmtNames_increaseCtxs,
      exactEval:host:stmtNames_increaseCtxs_ctxs,
      exactEval:host:exprNames_increaseCtxs. [Show Proof]



Prove_Constraint exactEval:host:proj_exprNames.
Prove_Constraint exactEval:host:proj_stmtNames. [Show Proof]

Prove_Constraint exactEval:host:proj_stmtNames_names_forward. [Show Proof]

Prove_Constraint exactEval:host:proj_stmtNames_names_backward. [Show Proof]





/********************************************************************
 Typing
 ********************************************************************/
Prove exactEval:host:typeOf_isTy,
      exactEval:host:stmtOK_isCtx. [Show Proof]



Prove exactEval:host:stmtOK_keep_scopes. [Show Proof]



Prove exactEval:host:stmtOK_older_scopes_same. [Show Proof]



Prove exactEval:host:stmtOK_first_scope_lookup_same. [Show Proof]



Prove exactEval:host:typeOf_unique,
      exactEval:host:stmtOK_unique. [Show Proof]



Prove exactEval:host:paramTy_is.
Prove exactEval:host:getFunInfo_is.


Prove exactEval:host:paramTy_exists.
Prove exactEval:host:getFunInfo_exists.




/********************************************************************
 Evaluation
 ********************************************************************/
Prove exactEval:host:evalExpr_isCtx,
      exactEval:host:evalExpr_isValue,
      exactEval:host:evalStmt_isCtx,
      exactEval:host:evalArgs_isCtx,
      exactEval:host:evalArgs_isValue,
      exactEval:host:evalRecFields_isCtx,
      exactEval:host:evalRecFields_isValue. [Show Proof]



Prove exactEval:host:evalExpr_isOutput,
      exactEval:host:evalStmt_isOutput,
      exactEval:host:evalArgs_isOutput,
      exactEval:host:evalRecFields_isOutput. [Show Proof]



Prove exactEval:host:paramName_is.
Prove exactEval:host:getFunEvalInfo_is.

Prove exactEval:host:evalProgram_isOutput.


Prove exactEval:host:evalExpr_names_same,
      exactEval:host:evalStmt_names_same,
      exactEval:host:evalArgs_names_same,
      exactEval:host:evalRecFields_names_same. [Show Proof]



Prove exactEval:host:evalExpr_newNameScopes,
      exactEval:host:evalExpr_newNameScopes_output,
      exactEval:host:evalExpr_newNameScopes_ctx,
      exactEval:host:evalStmt_newNameScopes_output,
      exactEval:host:evalStmt_newNameScopes,
      exactEval:host:evalArgs_newNameScopes,
      exactEval:host:evalArgs_newNameScopes_output,
      exactEval:host:evalArgs_newNameScopes_ctx,
      exactEval:host:evalRecFields_newNameScopes,
      exactEval:host:evalRecFields_newNameScopes_output,
      exactEval:host:evalRecFields_newNameScopes_ctx. [Show Proof]



Add_Ext_Size exactEval:host:evalExpr,
             exactEval:host:evalArgs,
             exactEval:host:evalRecFields,
             exactEval:host:evalStmt.
Add_Proj_Rel exactEval:host:evalExpr,
             exactEval:host:evalArgs,
             exactEval:host:evalRecFields,
             exactEval:host:evalStmt.


Prove exactEval:host:evalExpr_newNameScopes_exists_ES,
      exactEval:host:evalStmt_newNameScopes_exists_ES,
      exactEval:host:evalArgs_newNameScopes_exists_ES,
      exactEval:host:evalRecFields_newNameScopes_exists_ES. [Show Proof]



Prove exactEval:host:evalExpr_ctx_names,
      exactEval:host:evalStmt_ctx_names,
      exactEval:host:evalArgs_ctx_names,
      exactEval:host:evalRecFields_ctx_names. [Show Proof]



Prove exactEval:host:evalExpr_newNameScopes_exists_back,
      exactEval:host:evalStmt_newNameScopes_exists_back,
      exactEval:host:evalArgs_newNameScopes_exists_back,
      exactEval:host:evalRecFields_newNameScopes_exists_back. [Show Proof]



Prove exactEval:host:evalExpr_scopes_same,
      exactEval:host:evalExpr_scopes_same_ctx,
      exactEval:host:evalStmt_scopes_same,
      exactEval:host:evalStmt_scopes_same_ctx,
      exactEval:host:evalArgs_scopes_same,
      exactEval:host:evalArgs_scopes_same_ctx,
      exactEval:host:evalRecFields_scopes_same,
      exactEval:host:evalRecFields_scopes_same_ctx. [Show Proof]


Prove exactEval:host:evalExpr_scopes_same_exists,
      exactEval:host:evalStmt_scopes_same_exists,
      exactEval:host:evalArgs_scopes_same_exists,
      exactEval:host:evalRecFields_scopes_same_exists. [Show Proof]



Prove_Constraint exactEval:host:proj_evalExpr_forward.
Prove_Constraint exactEval:host:proj_evalExpr_backward.

Theorem is_list_values_append_nil : forall L,
  is_list is_value L -> L ++ [] = L. [Show Proof]


Prove_Constraint exactEval:host:proj_evalStmt_forward. [Show Proof]


Prove_Constraint exactEval:host:proj_evalStmt_backward. [Show Proof]



Prove_Ext_Ind exactEval:host:evalExpr,
              exactEval:host:evalArgs,
              exactEval:host:evalRecFields,
              exactEval:host:evalStmt. [Show Proof]



Prove exactEval:host:paramName_unique.
Prove_Constraint exactEval:host:proj_paramName_forward.
Prove_Constraint exactEval:host:proj_paramName_back.
Prove exactEval:host:getFunEvalInfo_unique.
Prove_Constraint exactEval:host:proj_getFunEvalInfo_forward.
Prove_Constraint exactEval:host:proj_getFunEvalInfo_back.

Prove exactEval:host:evalProgram_unique.
Prove_Constraint exactEval:host:proj_evalProgram_forward.
Prove_Constraint exactEval:host:proj_evalProgram_back.


Prove exactEval:host:evalExpr_typePres_ctx,
      exactEval:host:evalExpr_typePres,
      exactEval:host:evalStmt_typePres,
      exactEval:host:evalArgs_typePres_Ctx,
      exactEval:host:evalArgs_typePres,
      exactEval:host:evalRecFields_typePres_Ctx,
      exactEval:host:evalRecFields_typePres. [Show Proof]



Prove exactEval:host:paramTy_paramName_same.
Prove exactEval:host:funOK_getFunEvalInfo_related.


Prove exactEval:host:evalExpr_output_forms,
      exactEval:host:evalStmt_output_forms,
      exactEval:host:evalArgs_output_forms,
      exactEval:host:evalRecFields_output_forms. [Show Proof]



Prove exactEval:host:evalProgram_output_forms.


Prove exactEval:host:paramName_exists.
Prove exactEval:host:getFunEvalInfo_exists.
Back to example home