Changeset 321 for C-semantics
- Timestamp:
- Nov 26, 2010, 7:00:11 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/CexecIO.ma
r295 r321 1427 1427 1428 1428 (* 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.1429 ncoinductive 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 1432 ninductive 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'. 1434 1434 1435 1435 ninductive execution_matches_behavior: execution → program_behavior → Prop ≝ … … 1440 1440 execution_diverges tr e → 1441 1441 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 → 1444 1444 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' → 1447 1447 execution_matches_behavior e (Goes_wrong tr). 1448 1448 … … 1507 1507 ##] nqed. 1508 1508 1509 nlet 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 ≝ ?. 1513 ncut (∃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 ##] 1532 nqed. 1533 1534 (* is/needs completeness... 1535 nlemma 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; 1543 ncases (several_steps … ESTEPS EXEC); 1544 #STAR EXEC'; 1545 *) 1546 1509 1547 (* 1510 1548 ntheorem 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.