Changeset 295


Ignore:
Timestamp:
Nov 25, 2010, 6:15:47 PM (9 years ago)
Author:
campbell
Message:

Soundness of terminating whole program execution.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r291 r295  
    14121412##] nqed.
    14131413
    1414 ninductive execution_terminates : trace → int → execution → Prop ≝
     1414ninductive execution_terminates : trace → state → execution → state → Prop ≝
    14151415| terminates : ∀s,s',tr,tr',r,e,m.
    1416     execution_isteps tr s e s' (e_stop tr' r m) → execution_terminates (tr⧺tr') r e.
     1416    execution_isteps tr s e s' (e_stop tr' r m) → execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m).
    14171417
    14181418ncoinductive execution_diverging : execution → Prop ≝
     
    14341434
    14351435ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
    1436 | emb_terminates: ∀e,tr,r.
    1437     execution_terminates tr r e
     1436| emb_terminates: ∀s,s',e,tr,r.
     1437    execution_terminates tr s e s'
    14381438    execution_matches_behavior e (Terminates tr r)
    14391439| emb_diverges: ∀e,tr.
     
    14771477nqed.
    14781478
     1479nlemma final_step: ∀ge,tr,r,m,s.
     1480  exec_inf_aux ge (exec_step ge s) = e_stop tr r m →
     1481  step ge s tr (Returnstate (Vint r) Kstop m).
     1482#ge tr r m s;
     1483nrewrite > (exec_inf_aux_unfold …);
     1484nlapply (exec_step_sound ge s);
     1485ncases (exec_step ge s);
     1486##[ #o k H EXEC; nwhd in EXEC:(??%?); ndestruct
     1487##| #x; ncases x; #tr' s' SOUND; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
     1488    #FINAL EXEC; nwhd in SOUND EXEC:(??%?); ndestruct;
     1489    ncases FINAL; #r' FINAL'; ninversion FINAL';
     1490    #r'' m' E1 E2; ndestruct;
     1491    napply SOUND;
     1492##| #_; #EXEC; nwhd in EXEC:(??%?); ndestruct
     1493##] nqed.
     1494
     1495nlemma terminates_sound: ∀ge,tr,s,s',e.
     1496  execution_terminates tr s e s' →
     1497  exec_inf_aux ge (Value ??? 〈E0, s〉) = (e_step E0 s e) →
     1498  ∃r. star (mk_transrel … step) ge s tr s' ∧ final_state s' r.
     1499#ge tr0 s0 s0' e0 H; ncases H;
     1500#s s' tr tr' r e m ESTEPS EXEC; @r; @; //;
     1501ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
     1502napply (star_right … STARs');
     1503##[ ##2: napply (final_step ge tr' r m s');
     1504         napply (exec_e_step … EXECs');
     1505##| ##skip
     1506##| napply refl
     1507##] nqed.
     1508
    14791509(*
    14801510ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
Note: See TracChangeset for help on using the changeset viewer.