Talk:Predicate transformer semantics

A more in-depth discussion of if and do is required, as well as nondeterminism. Also, an example of how to use predicate transformers to derive a non-trivial algorithm might be good, as long as it doesn't conflict with policy. Also, the references section could use some filling out, specifically to the Gries' and Backhous' newer books on the subject. The relationship to predicate calculus could also be filled out. --jayinbmore 23:58, 31 Jan 2005 (UTC)

Also needs accounting of the wlp "weakest liberal precondition" predicate transformer. --jayinbmore 07:53, 1 Feb 2005 (UTC)

Have merged wlp into this article, as suggested in that article, but it could do with more detail PJTraill (talk) 18:14, 3 December 2009 (UTC)

Link to Assertion (computing)

The link of "predicate" to Assertion (computing) is rather unhelpful, but the article Predicate (mathematical logic), though more relevant is a mess, and perhaps not much more helpful. Can somebody do better? PJTraill (talk) 00:10, 23 November 2009 (UTC)

• I disagree re: the unhelpfulness of the link to Assertion (computing) since that's exactly what "predicate" means in the context of "predicate transformer semantics". --Jdinolt (talk) 21:28, 4 December 2009 (UTC)
  • Actually I retract. The page for Assertion (computing) has changed a lot since I initially put that link in. —Preceding unsigned comment added by Jdinolt (talk • contribs) 21:33, 4 December 2009 (UTC)
• In the meantime, I have changed the link. Of course, assertions (in the programming sense) are also worth linking too, but not at that particular point, I feel. —Preceding unsigned comment added by PJTraill (talk • contribs) 20:00, 6 December 2009 (UTC)

Expressions

The mathematical interpretation of several expressions is rather inobvious, for example $sp(x:=E,R)\ =\ \exists y,x=E[x\leftarrow y]\wedge R[x\leftarrow y]$. Is the right-hand-side a formula? Then why not use parenthesis or words, such as follows?

$sp(x:=E,R)$ is the formula $\exists y{\mbox{ s.t. }}x=E[x\leftarrow y]\land R[x\leftarrow y]$

I ask because I'm not certain I understand the formula as originally formatted. Diggory Hardy (talk) 17:48, 14 March 2012 (UTC)

The While case needs a partial correctness rule

Currently, only the total correctness rule for while is provided. The rule is (unavoidably) complex, and unfortunately obscures the essence of the weakest precondition semantics of while. Newcomers in particular will be scared away perhaps never to look at weakest preconditions again. If we remove the termination requirement, a much simpler rule emerges for the weakest liberal precondition, which I denote wlp

$wlp({\textbf {while}}\ E\ {\textbf {do}}\ S\ {\textbf {done}},R)\ =\ I\wedge \ ((E\wedge I)\Rightarrow wp(S,I))\wedge \ ((\neg E\wedge I)\Rightarrow R)\$

which simplifies even further to

$wlp({\textbf {while}}\ E\ {\textbf {do}}\ S\ {\textbf {done}},R)\ =\ I\wedge \ (E\Rightarrow wp(S,I))\wedge \ (\neg E\Rightarrow R)\$

This simply states that the invariant must always hold and additionally the invariant and guard taken together be strong enough to establish the postcondition, and at the end of the loop when the loop guard is false it together with the invariant should be able to establish the required postcondition.

If no one has any objections I will make the change to the page

Houseofwealth (talk) 00:56, 5 March 2015 (UTC)

Stongest postconditions are missing a motivation

Also a slightly better motivation for weakest preconditions could be given. Something along the lines of:

Given a program that needs to satisfy some condition when it has finished executing, what are the minimum conditions that need to hold prior to the program execution to ensure this?