fact: Definition prog_lost_ring: PProg := fun n => match n with | 0 => put (1, "I Lost my ring!");; put (1, "Nevermind -- I just found it. :)");; skip | 1 => post <- get (1);; if (string_dec post "Nevermind -- I just found it. :)") then put (2, "Glad to hear!");; skip else skip | 2 => postB <- get (2);; if (string_dec postB "Glad to hear!") then postA <- get (1);; if (string_dec postA "Nevermind -- I just found it. :)") then skip else fault else skip | _ => skip end%Prog.
imports: Coq(String) Chapar(Predefs KVStore ReflectiveAbstractSemantics)