Changeset 321


Ignore:
Timestamp:
Nov 26, 2010, 7:00:11 PM (9 years ago)
Author:
campbell
Message:

Soundness for reactive executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r295 r321  
    14271427
    14281428(* NB: "reacting" includes hitting a cost label. *)
    1429 ncoinductive execution_reacts : traceinf → execution → Prop ≝
    1430 | reacting: ∀tr,tr',s,s',e,e'. execution_reacts tr' e' → execution_isteps tr s e s' e' → tr ≠ E0 → execution_reacts (tr⧻tr') e.
    1431 
    1432 ninductive execution_goes_wrong: trace → execution → Prop ≝
    1433 | go_wrong: ∀tr,s,s',e. execution_isteps tr s e s' e_wrong → execution_goes_wrong tr e.
     1429ncoinductive execution_reacts : traceinf → state → execution → Prop ≝
     1430| reacting: ∀tr,tr',s,s',e,e'. execution_reacts tr' s' e' → execution_isteps tr s e s' e' → tr ≠ E0 → execution_reacts (tr⧻tr') s e.
     1431
     1432ninductive execution_goes_wrong: trace → state → execution → state → Prop ≝
     1433| go_wrong: ∀tr,s,s',e. execution_isteps tr s e s' e_wrong → execution_goes_wrong tr s e s'.
    14341434
    14351435ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
     
    14401440    execution_diverges tr e →
    14411441    execution_matches_behavior e (Diverges tr)
    1442 | emb_reacts: ∀e,tr.
    1443     execution_reacts tr e →
     1442| emb_reacts: ∀s,e,tr.
     1443    execution_reacts tr s e →
    14441444    execution_matches_behavior e (Reacts tr)
    1445 | emb_wrong: ∀e,tr.
    1446     execution_goes_wrong tr e
     1445| emb_wrong: ∀e,s,s',tr.
     1446    execution_goes_wrong tr s e s'
    14471447    execution_matches_behavior e (Goes_wrong tr).
    14481448
     
    15071507##] nqed.
    15081508
     1509nlet corec reacts_sound ge tr s e
     1510  (REACTS:execution_reacts tr s e)
     1511  (EXEC:exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e) :
     1512  forever_reactive (mk_transrel … step) ge s tr ≝ ?.
     1513ncut (∃s'.∃e'.∃tr'.∃tr''.execution_reacts tr'' s' e' ∧ execution_isteps tr' s e s' e' ∧ tr' ≠ E0 ∧ tr = tr'⧻tr'');
     1514##[ ninversion REACTS;
     1515    #tr0 tr' s0 s' e0 e' EREACTS ESTEPS REACTED E1 E2 E3; ndestruct (E2 E3);
     1516    @ s'; @ e'; @ tr0; @ tr'; @; ##[ @; ##[ @; //; ##| napply REACTED ##] ##| napply refl ##]
     1517##| *; #s'; *; #e'; *; #tr'; *; #tr'';
     1518    *; *; *; #REACTS' ESTEPS REACTED APPTR;
     1519(*    nrewrite > APPTR;*)
     1520    napply (match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]);
     1521    @;
     1522    ncases (several_steps … ESTEPS EXEC); #STEPS EXEC';
     1523    ##[ ##2: napply STEPS;
     1524    ##| ##skip
     1525    ##| napply REACTED
     1526    ##| napply reacts_sound;
     1527      ##[ ##2: napply REACTS';
     1528      ##| ##skip
     1529      ##| napply EXEC'
     1530      ##]
     1531    ##]
     1532nqed.
     1533
     1534(* is/needs completeness...
     1535nlemma wrong_sound: ∀ge,tr,s,s',e.
     1536  execution_goes_wrong tr s e s' →
     1537  exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e →
     1538  star (mk_transrel … step) ge s tr s' ∧
     1539  nostep (mk_transrel … step) ge s' ∧
     1540  (¬∃r. final_state s' r).
     1541#ge tr0 s0 s0' e0 WRONG; ncases WRONG;
     1542#tr s s' e ESTEPS EXEC;
     1543ncases (several_steps … ESTEPS EXEC);
     1544#STAR EXEC';
     1545*)
     1546
    15091547(*
    15101548ntheorem 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.