Extensibella Example: simple_imp:assert

Language Specification

File: assert.sos

[Reduce File] [Raw File]

Module simple_imp:assert

Builds on simple_imp:host

c ::= ...
    | assert(e)

------------------------ [Proj-Assert]
|{c}- assert(E) ~~> noop



typeOf G E boolTy
-------------------- [T-Assert]
typeOK G assert(E) G



eval_e G E trueVal
-------------------- [E-Assert]
eval_c G assert(E) G

Module simple_imp:assert.


Prove_Constraint simple_imp:host:proj_e_unique.


Prove_Constraint simple_imp:host:proj_e_is.


Prove_Constraint simple_imp:host:proj_rf_unique.


Prove_Constraint simple_imp:host:proj_rf_is.


Prove_Constraint simple_imp:host:proj_c_unique. [Show Proof]

%assert
 case Hyp1. search.


Prove_Constraint simple_imp:host:proj_c_is. [Show Proof]

%assert
 search.


Prove_Constraint simple_imp:host:proj_recFields_unique.


Prove_Constraint simple_imp:host:proj_recFields_is.


Prove_Constraint simple_imp:host:proj_ty_unique.


Prove_Constraint simple_imp:host:proj_ty_is.


Prove_Constraint simple_imp:host:proj_value_unique.


Prove_Constraint simple_imp:host:proj_value_is.


Prove simple_imp:host:vars_join,
      simple_imp:host:vars_rf_join.


Prove simple_imp:host:vars_unique,
      simple_imp:host:vars_rf_unique.


Prove_Constraint simple_imp:host:proj_e_vars_exist.


Prove_Constraint simple_imp:host:proj_e_vars.


Prove_Constraint simple_imp:host:proj_rf_vars_exist.


Prove_Constraint simple_imp:host:proj_rf_vars.


Prove simple_imp:host:vars_is,
      simple_imp:host:vars_rf_is.


Prove simple_imp:host:vars_exist,
      simple_imp:host:vars_rf_exist.


Prove simple_imp:host:typeOf_unique,
      simple_imp:host:typeRecFields_unique.


Prove simple_imp:host:typeOK_unique. [Show Proof]

%T-Assert
 case Ty2. search.


Prove_Constraint simple_imp:host:proj_eval_e.


Prove simple_imp:host:eval_e_unique,
      simple_imp:host:eval_rf_unique.


Prove simple_imp:host:update_rec_fields_unique.


Prove_Constraint simple_imp:host:proj_c_eval. [Show Proof]

%assert
 Ev: case Hyp1. search.


Add_Ext_Size simple_imp:host:eval_c.
Add_Proj_Rel simple_imp:host:eval_c.


Prove_Ext_Ind simple_imp:host:eval_c. [Show Proof]

%assert
 search.


Prove simple_imp:host:eval_c_unique. [Show Proof]

%E-Assert
 case Ev2. search.


Prove_Constraint simple_imp:host:proj_c_eval_results. [Show Proof]

%assert
 case Hyp1. case Hyp2. search.


Prove_Constraint simple_imp:host:proj_c_eval_results_back. [Show Proof]

%assert
 case Hyp1. case Hyp2. search.


Prove simple_imp:host:vars_eval_same_result,
      simple_imp:host:vars_equal_rf_same_result.