0
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ 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$. $\endgroup$ – David Richerby Oct 28 '16 at 15:30
  • $\begingroup$ 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? $\endgroup$ – Martin Berger Oct 30 '16 at 12:12
  • $\begingroup$ I am really confused. I am looking at the predicate transformer semantics by Dijkstra, but couldn't find the answer. $\endgroup$ – snnlankrdsm Oct 30 '16 at 22:24
  • $\begingroup$ and also.. Can someone explain me why a > b is not a strongest postcondition for the first one. $\endgroup$ – snnlankrdsm Oct 30 '16 at 22:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.