Content deleted Content added
Tag: |
|||
| (20 intermediate revisions by 11 users not shown) | |||
Line 1:
{{WikiProject banner shell|class=C|
{{WikiProject Computer science|importance=mid}}
{{WikiProject Computing|software=yes|importance=mid}}
}}
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 [[First-order_logic|predicate calculus]] could also be filled out.
--[[User:Jdinolt|jayinbmore]] 23:58, 31 Jan 2005 (UTC)
Line 11 ⟶ 15:
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? [[User:PJTraill|PJTraill]] ([[User talk: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". --[[User:Jdinolt|Jdinolt]] ([[User talk: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. <small><span class="autosigned">—Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[User:Jdinolt|Jdinolt]] ([[User talk:Jdinolt|talk]] • [[Special:Contributions/Jdinolt|contribs]]) 21:33, 4 December 2009 (UTC)</span></small><!-- Template:Unsigned --> <!--Autosigned by SineBot-->
* 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. <small><span class="autosigned">—Preceding [[Wikipedia:Signatures|unsigned]] comment added by [[User:PJTraill|PJTraill]] ([[User talk:PJTraill|talk]] • [[Special:Contributions/PJTraill|contribs]]) 20:00, 6 December 2009 (UTC)</span></small><!-- Template:Unsigned --> <!--Autosigned by SineBot-->
== Expressions ==
The mathematical interpretation of several expressions is rather inobvious, for example <math> sp(x := E, R)\ =\ \exists y, x=E[x \leftarrow y] \wedge R[x \leftarrow y]</math>. Is the right-hand-side a formula? Then why not use parenthesis or words, such as follows?
<math> sp(x := E, R)</math> is the formula <math>\exists y \mbox{ s.t. } x=E[x \leftarrow y] \land R[x \leftarrow y]</math>
I ask because I'm not certain I understand the formula as originally formatted. [[User:Diggory Hardy|Diggory Hardy]] ([[User talk: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
{| style="background-color:#eeeeff;" border="1" cellpadding="10"
|<math>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)
\ </math>
|}
which simplifies even further to
{| style="background-color:#eeeeff;" border="1" cellpadding="10"
|<math>wlp(\textbf{while}\ E\ \textbf{do}\ S\ \textbf{done}, R)\ =\
I \wedge\ (E \Rightarrow wp(S,I)) \wedge\ (\neg E \Rightarrow R)
\ </math>
|}
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
[[User:Houseofwealth|Houseofwealth]] ([[User talk:Houseofwealth|talk]]) 00:56, 5 March 2015 (UTC)
The middle clause of the wlp doesn't guarantee that the whole wlp is still true after the first iteration (when E is true at first), only the invariant, which makes it too weak.
For instance, with the following program and given some valid invariant I (just True?)
while x < 2 do x := x+1 done
The state <code>{x = 0}</code> should satisfy the wlp <math>I \wedge (E \Rightarrow I[x \leftarrow x+1]) \wedge (\neg E \Rightarrow R)</math>, for any tautology R, so the first and second clauses are true, and the last one is actually true independently of the value of R; so we can replace it with an unsatisfiable postcondition <math>(x = 42)</math>, and our wlp would still hold; even though it should never do, as the loop always terminates. A universal quantification like in the total correctness subsection seems necessary here as well. [[User:Syrak|Syrak]] ([[User talk:Syrak|talk]]) 22:41, 9 April 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?
[[User:Houseofwealth|Houseofwealth]] ([[User talk:Houseofwealth|talk]]) 01:12, 5 March 2015 (UTC)
== Strictness of wp depends on allowed statements ==
<p>If we allow an assume statement, the wp operator is not strict:<br>
The weakest precondition of False before the statement <code>assume !A</code> is exactly the formula that satisfies A.</p>
Assume statements are common in the field of software verification<ref name="ZeeKuncak2009">{{cite journal|last1=Zee|first1=Karen|last2=Kuncak|first2=Viktor|last3=Rinard|first3=Martin C.|title=An integrated proof language for imperative programs|journal=ACM SIGPLAN Notices|volume=44|issue=6|year=2009|pages=338|issn=03621340|doi=10.1145/1543135.1542514}}</ref>
In model checking, often a program is represented as a control flow graph.<ref name="ArltRümmer2013">{{cite journal|last1=Arlt|first1=Stephan|last2=Rümmer|first2=Philipp|last3=Schäf|first3=Martin|title=A Theory for Control-Flow Graph Exploration|volume=8172|year=2013|pages=506–515|issn=0302-9743|doi=10.1007/978-3-319-02444-8_44}}</ref>
<ref name="CytronFerrante1991">{{cite journal|last1=Cytron|first1=Ron|last2=Ferrante|first2=Jeanne|last3=Rosen|first3=Barry K.|last4=Wegman|first4=Mark N.|last5=Zadeck|first5=F. Kenneth|title=Efficiently computing static single assignment form and the control dependence graph|journal=ACM Transactions on Programming Languages and Systems|volume=13|issue=4|year=1991|pages=451–490|issn=01640925|doi=10.1145/115372.115320}}</ref>
For example a statement <pre> if A then C1 else C2 </pre>
is typically translated to a start ___location with two outgoing edges
to nodes that represent the entry to the representation of the subprograms C1 and C2.
The edge entering C1 is labeled <code>assume A</code> and the edge entering C2 <code>assume !A</code> respectively.
{{reflist-talk}}
| |||