Changeset 365


Ignore:
Timestamp:
Dec 2, 2010, 4:40:54 PM (9 years ago)
Author:
campbell
Message:

Soundness (really completeness) of Wrong executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r253 r365  
    485485##] nqed.
    486486 
     487nlemma wrong_sound: ∀ge,tr,s,s',e.
     488  execution_goes_wrong tr s e s' →
     489  exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e →
     490  star (mk_transrel … step) ge s tr s' ∧
     491  nostep (mk_transrel … step) ge s' ∧
     492  (¬∃r. final_state s' r).
     493#ge tr0 s0 s0' e0 WRONG; ncases WRONG;
     494#tr s s' e ESTEPS EXEC;
     495ncases (several_steps … ESTEPS EXEC);
     496#STAR EXEC'; @;
     497##[ @; ##[ napply STAR;
     498       ##| #badtr bads; @; #badSTEP;
     499           nlapply (step_complete … badSTEP);
     500           nlapply (exec_e_step … EXEC');
     501           ncases (exec_step ge s');
     502           ##[ #o k; nrewrite > (execution_cases (exec_inf_aux …)); #E; nwhd in E:(??%?);
     503               ndestruct
     504           ##| #x; ncases x; #trx stx; nrewrite > (exec_inf_aux_unfold …);
     505               nwhd in ⊢ (??%? → ?); ncases (is_final_state stx);
     506               #FINAL E; nwhd in E:(??%?); ndestruct
     507           ##| #E H; nwhd in H; napply H
     508           ##]
     509       ##]
     510##| @; #FINAL;
     511    nrewrite > (exec_inf_aux_unfold …) in EXEC';
     512    nwhd in ⊢ (??%? → ?);
     513    ncases (is_final_state s'); #FINAL';
     514    ##[ nwhd in ⊢ (??%? → ?); #E; ndestruct;
     515    ##| napply False_ind; napply (absurd … FINAL FINAL');
     516    ##]
     517##] nqed.
Note: See TracChangeset for help on using the changeset viewer.