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?