# What does “post-image analysis” mean in the context of formal program analysis?

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}$.