![]() | This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | |||||||||||||||||
|
I would like to know in what articles I can find the reference from which the Conditional Rule and the extended Iteration Rule (for total correctness) have been taken, because they are not in the original article by Hoare.-- 189.4.49.11 ( talk) 22:08, 9 April 2013 (UTC)
Shouldnt the right hand side of the assignment axiom be {P[x]}?
I believe this is unclear:
The intuitive reading of such a triple is: Whenever P holds of the state before the execution of C, then Q will hold afterwards. Note that if C does not terminate, then there is no "after", so Q can be any statement at all. Indeed, one can choose Q to be false to express that C does not terminate. This is called "partial correctness". If C terminates and at termination Q is true, the expression exhibits "total correctness". Termination would have to be proved separately.
"This" refers to something in the preceeding paragraph and is therefore unclear. Why isn't this much better?
The intuitive reading of such a triple is: Whenever P holds of the state before the execution of C, then Q will hold afterwards. Note that if C does not terminate, then there is no "after", so Q can be any statement at all. Indeed, one can choose Q to be false to express that C does not terminate; this is called "partial correctness". If C terminates and at termination Q is true, the expression exhibits "total correctness". Termination would have to be proved separately.
This put the explaination right in with the thing being explained. Comments? Rangek 16:51, 9 August 2006 (UTC)
I am confused on this point:
is not a true statement, because no precondition can cause y to be 3 after x is set to 2.
Since the precondition states that y is set to 3, and the operation does not change y, then it seems that y should remain equal to 3, meaning that the statement is true.
This means that I have it wrong, or the statement is incorrect. If it's incorrect, then it needs to be changed. If I have it wrong then perhaps it needs to be explained more clearly? —Preceding unsigned comment added by Gearon ( talk • contribs)
Some of the examples in this article do not match well with the exercises in Hoare logic I was given in University. It is not that they are incorrect per se, but the pedagogical value of them may be questioned. For example, under the section "Sequencing rule" is written:
For example, consider the following two instances of the assignment axiom:
and
By the sequencing rule, one concludes:
Which I feel could be better expressed in this more educational and also more practically applicable manner:
For example, consider the following two instances of the assignment axiom:
and
By the sequencing rule, one concludes:
Heathhunnicutt 18:12, 22 January 2007 (UTC)
how about repeat C until B rules
Imho, a critical point regarding notation is unclear: Somewhere in the middle, the article starts writing a bar with something above it and something below. Although the source code uses "\frac{}", I seriously doubt that those are proper fractions. It must mean something like "if numerator then denominator", "numerator implies denominator", but that's a guess. Explaining it should only take a sentence or two, but it's important to do that since I can't seem to find that notation in Hoare's original paper (see References section) or any other WP page in the category. Thanks in advance. -- 193.99.145.162 17:57, 12 March 2007 (UTC)
Correct me if I am wrong, but aren't only the free occurences of the variables in the statement, should be replaced during the partical correctnees? —Preceding unsigned comment added by 70.179.134.208 ( talk) 18:34, 12 September 2007 (UTC)
A sentence or two on completenes would be appreciated. Does every correct Hoare triple have a derivation in Hoare Logic? How about function calls, gotos, mallocs, and the like? (Without mallocs, the language is not Turing complete, unless perhaps we assume that the variables range over an infinite domain.) 129.27.152.212 ( talk) 08:36, 24 November 2008 (UTC)
It's not clear from our description of the "While rule for total correctness" why t couldn't just keep decreasing forever, thereby ruining the termination proof. Can someone provide an explanation? -- Doradus ( talk) 15:28, 28 August 2009 (UTC)
Everything seems inverted in this article,
And
doesn't look logical to me, shouldn't it be:
Rursus dixit. ( mbork3!) 07:32, 24 October 2011 (UTC)
I agree. Going to start changing.
DuckMaestro (
talk) 00:39, 25 February 2012 (UTC)
Perhaps something is wrong in my browser, perhaps I don't understand how wiki works, but whenever I try to edit the dead link which reference Robert Floyd's work, by posting the one available in his main article: http://www.cs.virginia.edu/~weimer/2007-615/reading/FloydMeaning.pdf , the whole reference section appears blank to me.
I click edit and the reference section is completely empty. So if someone can explain why this happens... I would be grateful.
Because I'd rather not lose the whole section and rewrite it manually since I only planned to fix a dead link. Kharazyr ( talk) 22:29, 8 January 2012 (UTC)
Kharazyr ( talk) 18:21, 16 January 2012 (UTC)
If < is well ordering of D and S transfers machine from a state satisfyng P and B and t is in D and t=z into state satisfyng P and t is in D and t<z, then while B do S transfers machine from a state satysfing P and (B implies t is in D) into state satisfyng P and not B. The concluding triple is incorrect about conditions of a machine state before the loop. — Preceding unsigned comment added by 212.200.65.82 ( talk) 20:51, 27 November 2013 (UTC)
int
expression, to prove termination we need to know at the start of every loop cycle that t didn't get negative, i.e. that it is still in D. -
Jochen Burghardt (
talk) 19:04, 28 November 2013 (UTC)Let
- D={1,2},
- < is usual order on integers,
- P is truth,
- t=x,
- B is "x>1",
- S is "if x<3 then x=x-1"
then
1. < is well ordering on the set D,
2. P and B and (t in D) and t=z simultaneously holds if and only if x=z=2. In this case, after executing S holds x=1 and z=2 ant it implies that P and (t in D) and t<z. Also, S is executed in the finite time.
3. If x=3 then P holds, but "while B do S done" never terminates.
I've never studied Hoare Logic, so I'm posting here to ensure that I'm correct before making the edit.
In the section about "Assignment axiom schema", in the paragraph beginning "While a given postcondition P uniquely determines the precondition...", I'm confused about why the examples listed are valid. Earlier, the description of replacement process is that "x := E" leads to "each free occurrence of x has been replaced by the expression E", but in this case, y * y is the expression, but y * y is being replaced with x.
However, if the precondition were
{ 0 ≤ x ∧ x ≤ 9 }
and the command
x := y * y
then there would only be one valid postcondition, since every instance of the free variable has to be replaced
{ 0 ≤ y * y ∧ y * y ≤ 9 }
Hello fellow Wikipedians,
I have just modified one external link on Hoare logic. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.
This message was posted before February 2018.
After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than
regular verification using the archive tool instructions below. Editors
have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the
RfC before doing mass systematic removals. This message is updated dynamically through the template {{
source check}}
(last update: 5 June 2024).
Cheers.— InternetArchiveBot ( Report bug) 16:27, 5 November 2017 (UTC)
![]() | This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | |||||||||||||||||
|
I would like to know in what articles I can find the reference from which the Conditional Rule and the extended Iteration Rule (for total correctness) have been taken, because they are not in the original article by Hoare.-- 189.4.49.11 ( talk) 22:08, 9 April 2013 (UTC)
Shouldnt the right hand side of the assignment axiom be {P[x]}?
I believe this is unclear:
The intuitive reading of such a triple is: Whenever P holds of the state before the execution of C, then Q will hold afterwards. Note that if C does not terminate, then there is no "after", so Q can be any statement at all. Indeed, one can choose Q to be false to express that C does not terminate. This is called "partial correctness". If C terminates and at termination Q is true, the expression exhibits "total correctness". Termination would have to be proved separately.
"This" refers to something in the preceeding paragraph and is therefore unclear. Why isn't this much better?
The intuitive reading of such a triple is: Whenever P holds of the state before the execution of C, then Q will hold afterwards. Note that if C does not terminate, then there is no "after", so Q can be any statement at all. Indeed, one can choose Q to be false to express that C does not terminate; this is called "partial correctness". If C terminates and at termination Q is true, the expression exhibits "total correctness". Termination would have to be proved separately.
This put the explaination right in with the thing being explained. Comments? Rangek 16:51, 9 August 2006 (UTC)
I am confused on this point:
is not a true statement, because no precondition can cause y to be 3 after x is set to 2.
Since the precondition states that y is set to 3, and the operation does not change y, then it seems that y should remain equal to 3, meaning that the statement is true.
This means that I have it wrong, or the statement is incorrect. If it's incorrect, then it needs to be changed. If I have it wrong then perhaps it needs to be explained more clearly? —Preceding unsigned comment added by Gearon ( talk • contribs)
Some of the examples in this article do not match well with the exercises in Hoare logic I was given in University. It is not that they are incorrect per se, but the pedagogical value of them may be questioned. For example, under the section "Sequencing rule" is written:
For example, consider the following two instances of the assignment axiom:
and
By the sequencing rule, one concludes:
Which I feel could be better expressed in this more educational and also more practically applicable manner:
For example, consider the following two instances of the assignment axiom:
and
By the sequencing rule, one concludes:
Heathhunnicutt 18:12, 22 January 2007 (UTC)
how about repeat C until B rules
Imho, a critical point regarding notation is unclear: Somewhere in the middle, the article starts writing a bar with something above it and something below. Although the source code uses "\frac{}", I seriously doubt that those are proper fractions. It must mean something like "if numerator then denominator", "numerator implies denominator", but that's a guess. Explaining it should only take a sentence or two, but it's important to do that since I can't seem to find that notation in Hoare's original paper (see References section) or any other WP page in the category. Thanks in advance. -- 193.99.145.162 17:57, 12 March 2007 (UTC)
Correct me if I am wrong, but aren't only the free occurences of the variables in the statement, should be replaced during the partical correctnees? —Preceding unsigned comment added by 70.179.134.208 ( talk) 18:34, 12 September 2007 (UTC)
A sentence or two on completenes would be appreciated. Does every correct Hoare triple have a derivation in Hoare Logic? How about function calls, gotos, mallocs, and the like? (Without mallocs, the language is not Turing complete, unless perhaps we assume that the variables range over an infinite domain.) 129.27.152.212 ( talk) 08:36, 24 November 2008 (UTC)
It's not clear from our description of the "While rule for total correctness" why t couldn't just keep decreasing forever, thereby ruining the termination proof. Can someone provide an explanation? -- Doradus ( talk) 15:28, 28 August 2009 (UTC)
Everything seems inverted in this article,
And
doesn't look logical to me, shouldn't it be:
Rursus dixit. ( mbork3!) 07:32, 24 October 2011 (UTC)
I agree. Going to start changing.
DuckMaestro (
talk) 00:39, 25 February 2012 (UTC)
Perhaps something is wrong in my browser, perhaps I don't understand how wiki works, but whenever I try to edit the dead link which reference Robert Floyd's work, by posting the one available in his main article: http://www.cs.virginia.edu/~weimer/2007-615/reading/FloydMeaning.pdf , the whole reference section appears blank to me.
I click edit and the reference section is completely empty. So if someone can explain why this happens... I would be grateful.
Because I'd rather not lose the whole section and rewrite it manually since I only planned to fix a dead link. Kharazyr ( talk) 22:29, 8 January 2012 (UTC)
Kharazyr ( talk) 18:21, 16 January 2012 (UTC)
If < is well ordering of D and S transfers machine from a state satisfyng P and B and t is in D and t=z into state satisfyng P and t is in D and t<z, then while B do S transfers machine from a state satysfing P and (B implies t is in D) into state satisfyng P and not B. The concluding triple is incorrect about conditions of a machine state before the loop. — Preceding unsigned comment added by 212.200.65.82 ( talk) 20:51, 27 November 2013 (UTC)
int
expression, to prove termination we need to know at the start of every loop cycle that t didn't get negative, i.e. that it is still in D. -
Jochen Burghardt (
talk) 19:04, 28 November 2013 (UTC)Let
- D={1,2},
- < is usual order on integers,
- P is truth,
- t=x,
- B is "x>1",
- S is "if x<3 then x=x-1"
then
1. < is well ordering on the set D,
2. P and B and (t in D) and t=z simultaneously holds if and only if x=z=2. In this case, after executing S holds x=1 and z=2 ant it implies that P and (t in D) and t<z. Also, S is executed in the finite time.
3. If x=3 then P holds, but "while B do S done" never terminates.
I've never studied Hoare Logic, so I'm posting here to ensure that I'm correct before making the edit.
In the section about "Assignment axiom schema", in the paragraph beginning "While a given postcondition P uniquely determines the precondition...", I'm confused about why the examples listed are valid. Earlier, the description of replacement process is that "x := E" leads to "each free occurrence of x has been replaced by the expression E", but in this case, y * y is the expression, but y * y is being replaced with x.
However, if the precondition were
{ 0 ≤ x ∧ x ≤ 9 }
and the command
x := y * y
then there would only be one valid postcondition, since every instance of the free variable has to be replaced
{ 0 ≤ y * y ∧ y * y ≤ 9 }
Hello fellow Wikipedians,
I have just modified one external link on Hoare logic. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.
This message was posted before February 2018.
After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than
regular verification using the archive tool instructions below. Editors
have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the
RfC before doing mass systematic removals. This message is updated dynamically through the template {{
source check}}
(last update: 5 June 2024).
Cheers.— InternetArchiveBot ( Report bug) 16:27, 5 November 2017 (UTC)