fact: Definition prog_photo_album: PProg := fun n => match n with | 0 => put (1, "uploads photos");; put (2, "creates album");; put (3, "adds photos to album");; skip | 1 => z <- get (3);; y <- get (2);; x <- get (1);; assert (if string_beq z "adds photos to album" then string_beq y "creates album" else true);; assert (if string_beq y "creates album" then string_beq x "uploads photos" else true);; skip | _ => skip end%Prog.
imports: Coq(String) Chapar(Predefs KVStore ReflectiveAbstractSemantics)