I am reviewing an anonymous paper about a sort of static analysis of programs that uses the phrase "post-image analysis", or "post-image operation" without defining what that is. I am guessing it is a well-known concept in formal methods, even though a Google search has not revealed anything.

I am guessing it means an analysis of the trace of a segment of a program. Basically, you run it a little bit, you collect the trace (perhaps that's a synonym for "image"), and analyse. But I am just guessing.

Can anyone tell me what that is, or give me a pointer?


When working with transition systems, $\text{post}(s)$ is the set of states that are reachable in a single step from the state $s$; if $S$ is a set of states,

$$\text{post}(S) = \bigcup_{s \in S} \text{post}(S).$$

Also, $\text{post}^*(s)$ is the set of states that are reachable from $s$, i.e., $\text{post}^*$ is the transitive closure of $\text{post}$.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.