# How can I find the strongest postcondition for those two Hoare triples?

I'm trying to solve an exercise in which I have to find the strongest post-condition of the two Hoare triples.

\begin{gather*} (| a=9 |)\ a=2; b=a+1; a=b*b;\ (| ?? |)\\ (| i=-j |)\ i=i+1; j=j-1;\ (| ?? |) \end{gather*} For the first one, I found post condition as $a > b$. For the second one, I found $j = |i|$. However, it seems like they are not the strongest. What are the strongest postconditions for those triples and why?

• Did you check the definition of strongest postcondition? Note that $j=|i|$ isn't even a postcondition (let alone a strongest one): consider running the code fragment starting with $i=1$, $j=-1$. – David Richerby Oct 28 '16 at 15:30
• There is no single strongest post-condition: if $P$ is a strongest post-condition, then so is e.g. $P \wedge 2=2$. More importantly, the answer to your question depends on the exact nature of the programming language that you use. For example: can variables be aliased? – Martin Berger Oct 30 '16 at 12:12
• I am really confused. I am looking at the predicate transformer semantics by Dijkstra, but couldn't find the answer. – snnlankrdsm Oct 30 '16 at 22:24
• and also.. Can someone explain me why a > b is not a strongest postcondition for the first one. – snnlankrdsm Oct 30 '16 at 22:27