fact: Definition prog_photo_upload: PProg := fun n => match n with | 0 => put (Photo, "NewPhoto");; put (Post, "Uploaded");; skip | 1 => post <- get (Post);; if (string_dec post "Uploaded") then photo <- get (Photo);; if string_dec photo "" then fault else skip else skip | _ => skip end%Prog.
imports: Coq(String) Chapar(Predefs KVStore ReflectiveAbstractSemantics)