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?

$\endgroup$

closed as off-topic by D.W., Raphael, Jan Johannsen, Lev Reyzin Sep 22 '17 at 14:54

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "Our site policy prohibits simultaneous crossposting: it duplicates effort and fractures discussion. Crossposting is permitted after a week has passed without a satisfying answer elsewhere. When crossposting please summarize the relevant discussions from other sites in your question and link between the copies in both directions." – D.W., Raphael, Jan Johannsen, Lev Reyzin
If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\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. Sep 21 '17 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 Sep 21 '17 at 22:17
  • $\begingroup$ Perhaps delete this one. It's not a research-level question. $\endgroup$ – Kai Sep 21 '17 at 22:40
  • $\begingroup$ Do you know any source where I can read about it? It is for research :) $\endgroup$ – blk Sep 21 '17 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 Sep 22 '17 at 0:32