The converse construct allows us to express facts about states preceding the current one and to reason backward about programs. For instance, [α-1]A means that before executing α, A had to hold. -1&gt;A can also be interpreted as the strongest post-condition to hold after the termination of a program &alpha; started in a world satisfying A.-->  We have