Extensibella Example: simple_imp:repeatWhile

Language Specification

File: repeatWhile.sos

[Reduce File] [Raw File] 
Module simple_imp:repeatWhile

Builds on simple_imp:host

/*Add a repeat-while construct*/
c ::= ...
    | repeatWhile(c, e)


------------------------------------- [Proj-RepeatWhile]
|{c}- repeatWhile(Body, Cond) ~~>
         seq(Body, while(Cond, Body))



/*Evaluation*/

eval_c G Body G1
eval_e G1 Cond trueVal
eval_c G1 repeatWhile(Body, Cond) G2
------------------------------------ [E-RepeatWhileTrue]
eval_c G repeatWhile(Body, Cond) G2


eval_c G Body G1
eval_e G1 Cond falseVal
----------------------------------- [E-RepeatWhileFalse]
eval_c G repeatWhile(Body, Cond) G1



/*Typing*/

typeOK G Body GB
typeOf G E boolTy
---------------------------------- [T-RepeatWhile]
typeOK G repeatWhile(Body, Cond) G
/*body opens a new scope*/

Reasoning

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

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

Module simple_imp:repeatWhile.


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]


Prove_Constraint simple_imp:host:proj_c_is. [Show Proof]



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]



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.


Theorem repeatWhile_projEval : forall G Body Cond G1,
    eval_c G (repeatWhile Body Cond) G1 ->
    exists G2, eval_c G (seq Body (while Cond Body)) G2. [Show Proof]


Prove_Constraint simple_imp:host:proj_c_eval. [Show Proof]



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


Theorem RW_to_SW: forall C B EG EG' N,
  <eval_c {ES}> EG (repeatWhile B C) EG' N ->
  exists N', <eval_c {ES}> EG (seq B (while C B)) EG' N' /\ N' < N. [Show Proof]



Prove_Ext_Ind simple_imp:host:eval_c. [Show Proof]



Prove simple_imp:host:eval_c_unique. [Show Proof]



Theorem repeatWhile_projSame : forall G Body Cond G1 G2,
    eval_c G (repeatWhile Body Cond) G1 ->
    eval_c G (seq Body (while Cond Body)) G2 ->
    G1 = G2. [Show Proof]


Prove_Constraint simple_imp:host:proj_c_eval_results. [Show Proof]



Prove_Constraint simple_imp:host:proj_c_eval_results_back. [Show Proof]



Prove simple_imp:host:vars_eval_same_result,
      simple_imp:host:vars_equal_rf_same_result.
Back to example home