1
$\begingroup$

The weakest precondition of while loop $\mathtt{while}(G)\{C\}$ with respect to postcondition $P$ can be characterized by the least fixed point of the predicate transformer

$X ~\mapsto \neg G \wedge P ~\vee~ G \wedge \mathsf{wp}(C, X)$

where $\mathsf{wp}(C, X)$ is the weakest precondition of loop body $C$ with respect to postcondition $X$.

How can strongest postconditions of while loops be defined/characterized in a similar fashion, i.e. given a precondition $Q$ and a predicate transformer $\mathsf{sp}(C, {\cdot})$, how can one characterize the strongest postcondition of $\mathtt{while}(G)\{C\}$ with respect to precondition $Q$ as a fixed point of some predicate transformer?

Improve this question
$\endgroup$
7
  • $\begingroup$ Cross-posted: cs.stackexchange.com/q/81493/755, cstheory.stackexchange.com/q/39140/5038. Please do not post the same question on multiple sites. Each community should have an honest shot at answering without anybody's time being wasted. $\endgroup$
    – D.W.
    Commented Sep 21, 2017 at 21:21
  • $\begingroup$ Sorry, I did not know and was not sure where to best place this question. Nevertheless, "Please do not post the same question on multiple sites. Each community should have an honest shot at answering without anybody's time being wasted." seems to contradict itself. What should I do? Delete one of the questions? $\endgroup$
    – blk
    Commented Sep 21, 2017 at 22:17
  • $\begingroup$ Perhaps delete this one. It's not a research-level question. $\endgroup$
    – Kai
    Commented Sep 21, 2017 at 22:40
  • $\begingroup$ Do you know any source where I can read about it? It is for research :) $\endgroup$
    – blk
    Commented Sep 21, 2017 at 22:44
  • $\begingroup$ @blk, if you have access, or are willing to purchase, this book has very good definition and example of sp and wp and how to use them. Although there probably are other free online sources that may be better. $\endgroup$
    – ryan
    Commented Sep 22, 2017 at 0:32

0

Reset to default