<p>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</p>

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

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

<p>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?</p>

CC BY-SA 3.0
2017-09-21T21:21:26.103Z
Cross-posted: https://cs.stackexchange.com/q/81493/755, https://cstheory.stackexchange.com/q/39140/5038.  Please [do not post the same question on multiple sites](https://meta.stackexchange.com/q/64068). Each community should have an honest shot at answering without anybody's time being wasted.
D.W.
CC BY-SA 3.0
2017-09-21T22:17:43.547Z
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?
blk
CC BY-SA 3.0
2017-09-21T22:40:15.133Z
Perhaps delete this one. It's not a research-level question.
Kai
CC BY-SA 3.0
2017-09-21T22:44:52.227Z
Do you know any source where I can read about it? It is for research :)
blk
CC BY-SA 3.0
2017-09-22T00:32:03.303Z
@blk, if you have access, or are willing to purchase, [this book](https://link.springer.com/book/10.1007%2F978-3-540-74113-8) 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.
ryan
CC BY-SA 3.0
2017-09-22T08:38:31.623Z
@ryan I don't support your book recommendation. The authors do not go into the details of what can and cannot be expressed by way of fixed points. I didn't find an answer to the question in it. On the other hand, [Dijkstra & Scholten's book](https://link.springer.com/book/10.1007%2F978-1-4612-3228-5) is probably a better choice. De Bakker's book ("Mathematical theory of program correctness", Prentice Hall, 1980) has answers to the question but it may be hard to find.
Kai
CC BY-SA 3.0
2017-10-02T14:07:26.867Z
Thank you, @Kai, your last comment really helped. If anyone's interested: According to de Bakker, there is no such fixed point characterization, see page 100, Theorem 3.36 and the preceding words. See also Remark 1. on page 101. Unfortunately, I cannot add this information as an answer to this question.
blk
<lo.logic><pl.programming-languages><program-verification>
Definitions of strongest postconditions
blk
# Definitions of strongest postconditions

(Asked by: username_0 on 2017-09-21)

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?

**Tags:** lo.logic, pl.programming-languages, program-verification
> **Comments:**
> **username_1**: Cross-posted: https://cs.stackexchange.com/q/81493/755, https://cstheory.stackexchange.com/q/39140/5038.  Please [do not post the same question on multiple sites](https://meta.stackexchange.com/q/64068). Each community should have an honest shot at answering without anybody's time being wasted.  
> **username_0**: 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?  
> **username_2**: Perhaps delete this one. It's not a research-level question.  
> **username_0**: Do you know any source where I can read about it? It is for research :)  
> **username_3**: @blk, if you have access, or are willing to purchase, [this book](https://link.springer.com/book/10.1007%2F978-3-540-74113-8) 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.  
> **username_2**: @ryan I don't support your book recommendation. The authors do not go into the details of what can and cannot be expressed by way of fixed points. I didn't find an answer to the question in it. On the other hand, [Dijkstra & Scholten's book](https://link.springer.com/book/10.1007%2F978-1-4612-3228-5) is probably a better choice. De Bakker's book ("Mathematical theory of program correctness", Prentice Hall, 1980) has answers to the question but it may be hard to find.  
> **username_0**: Thank you, @Kai, your last comment really helped. If anyone's interested: According to de Bakker, there is no such fixed point characterization, see page 100, Theorem 3.36 and the preceding words. See also Remark 1. on page 101. Unfortunately, I cannot add this information as an answer to this question.  

---

## 0 answers

