Ignore:
Timestamp:
Nov 23, 2012, 3:47:22 PM (7 years ago)
Author:
campbell
Message:

Set up "after_n_steps" to enforce an invariant on states.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2468 r2487  
    27572757  switch_state_sim ge s1 s1' →
    27582758  exec_step ge s1 = Value … 〈tr,s2〉 → 
    2759   ∃n. after_n_steps (S n) … clight_exec ge' s1'
     2759  ∃n. after_n_steps (S n) … clight_exec ge' s1' (λ_. true)
    27602760  (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2').
    27612761#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state
Note: See TracChangeset for help on using the changeset viewer.