Definition. Strongest Postcondition [005c]
Definition. Strongest Postcondition [005c]
In the most straightforward sense the strongest postcondition, denoted \(\texttt {sp}\) or \(\texttt {post}\), denotes the exact or least set of final states which we land in after a successful execution. Set theoretically we can denote it as.
\[ \texttt {sp}(s, P) = \{\sigma \in \Sigma \mid \exists \sigma ' \in \Sigma : \sigma ' \vDash P \land (s, \sigma ') \Downarrow \sigma \} \]We can also use a more logic way of expressing it as follows
\[ \texttt {sp}(s, P) \triangleq \exists \sigma '.\ P(\sigma ') \land (s, \sigma ') \Downarrow \sigma \]But the idea is in principle the same, it represents the set of states corresponding to some evaluated result based on some existing safe state.