Talk:Hoare logic

Citation Needed

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)

I added a remark about the missing conditional rule in Hoare's original, but I don't have sources for the rule(s) either. Jochen Burghardt (talk) 19:23, 24 May 2013 (UTC)

I found the conditional rule in this article, so i will add it as a source https://doi.org/10.1007/s00165-019-00501-3. I think the extended iteration rule may also be mentioned later, but I dont have time to check right now 79.146.32.217 (talk) 23:32, 3 November 2022 (UTC)

Old question

Shouldnt the right hand side of the assignment axiom be {P[x]}?

No, P is a formula of FOL in which x may occur. ---- Charles Stewart 17:00, 1 Feb 2005 (UTC)

Unclear

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)

You have managed to resolve the ambiguity by turning it into nonsense. I've rewritten the paragraph. Leibniz 20:17, 9 August 2006 (UTC)

I fail to see how my edit was nonsense, but your rewrite is better anyway. Rangek 20:38, 9 August 2006 (UTC)

Assignment Axiom

I am confused on this point:

$\{y=3\}x:=2\{y=3\}$

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)

The point you are missing is that the first part of the sentence you quoted said that x and y are aliases for the same location, so after executing "x := 2", y will have value 2 as well. -- Four Dog Night 02:58, 3 October 2006 (UTC)

Example of Rules Applications

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:

${\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}\!$

For example, consider the following two instances of the assignment axiom:

$\{x+1=43\}\ y:=x+1\ \{y=43\}$

and

$\{y=43\}\ z:=y\ \{z=43\}$

By the sequencing rule, one concludes:

$\{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}$

Which I feel could be better expressed in this more educational and also more practically applicable manner:

${\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}\!$

For example, consider the following two instances of the assignment axiom:

$\{x=42\}\ y:=x+1\ \{x=42\land y=43\}$

and

$\{y=43\}\ z:=y\ \{y=43\land z=43\}$

By the sequencing rule, one concludes:

$\{x=42\}\ y:=x+1;z:=y\ \{x=42\land y=43\land z=43\}$

Heathhunnicutt 18:12, 22 January 2007 (UTC)

how about repeat C until B rules

how about repeat C until B rules

Well, that isn't part of Hoare's paper. In fact, program verification texts usually only present one form of a particular construct, such as a while() loop. As another example, the texts usually present an if/else construct, but not a switch/case construct. The main issue here is that it is very important not to needlessly multiply all the mathematical statements you must refer to from the Hoare logic. Another way of putting this is that a paper like Hoare's but which covers all the constructs in a popular language would be really long, redundant, and hard to get the gist of.

To handle a do C until B write it as do C until not B which is the same as C; while (not B) do C;

All the program constructs available in a modern language except throw/catch can be transformed into the programming constructs covered by Hoare. Heathhunnicutt 17:08, 5 March 2007 (UTC)

What's with the fraction business?

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)

I was coming here to say exactly the same thing. The notation should be explained. I'll put an appropriate tag on the article - just got to work out which one. --Tango 23:47, 14 March 2007 (UTC)

I added an "expand section" template. StormWillLaugh (talk) 20:46, 28 December 2013 (UTC)

I tried to give an explanation in the footnote in the Hoare logic#Empty statement axiom schema section. However, the <math>...</math> parts do not render very well in the footnote popup box in my browser. If somebody has an idea how to replace "\frac{}{}" by wiki markup without <math>, please let me know. When the footnote is eventually considered a sufficient explanation, the "expand section" template should be removed. - Jochen Burghardt (talk) 15:40, 29 December 2013 (UTC)

Today, I replaced "\frac{}{}" by the "sfrac" template, and any other <math> stuff by unicode (hope I didn't introduce too much new typos). I also removed the "expand section" template. - Jochen Burghardt (talk) 11:04, 10 January 2014 (UTC)

free occurences

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)

When trying to improve the article along the issues from this talk page, I found that I don't understand your question: Which "statement" do you mean? What do you sugggest to "be replaced"? What does "during ... correctness" mean? Jochen Burghardt (talk) 19:32, 24 May 2013 (UTC)

Completeness

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)

Well, let's not get ahead of ourselves there. Even with mallocs, C is not turing complete because no real program can use a truly unlimited amount of storage. --Doradus (talk) 15:41, 28 August 2009 (UTC)

I agree to Doradus' remark on Turing completeness. However, the question of completeness of Hoare's calculus remains. As far as I know, this issue wasn't relevant in Hoare's original publication, as he axiomatically (cf. its title) defined the semantics of his toy programming language by his calculus. But when the Hoare calculus is applied to other languages, like C, someone has to prove that the Hoare calculus is consistent with the language semantics (as defined e.g. by Kernighan+Ritchie). Jochen Burghardt (talk) 17:51, 24 May 2013 (UTC)

Termination

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)

@Doradus I just asked this question at SO today. The jargon below the while-rule is hard to swallow, so I ignored it. Jameshfisher (talk) 18:33, 31 May 2011 (UTC)

I added some explanations about that in the article. (Hope they are of any help.) Jochen Burghardt (talk) 19:11, 24 May 2013 (UTC)

Inverted?

Everything seems inverted in this article,

this article: {P}Q{R}

Hoare's article: P{Q}R

And

this article: {P[E/x]}x:=E{P}

doesn't look logical to me, shouldn't it be:

maybe correct?: P{x:=E}P[E/x]

Rursus dixit. (^mbork³!) 07:32, 24 October 2011 (UTC)

Here is Hoare's article for anyone to read. See pages 577-579! Rursus dixit. (^mbork³!) 19:47, 17 December 2011 (UTC)

I agree. Going to start changing. DuckMaestro (talk) 00:39, 25 February 2012 (UTC)

I added a footnote to mention the inversion of "{P}Q{R}" in the original. The assignment rule "{P[E/x]}x:=E{P}" is correct, but "P{x:=E}P[E/x]" is wrong; as is now explained in the article with an example. Jochen Burghardt (talk) 19:20, 24 May 2013 (UTC)

References

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)

Never mind, I figured it out: the references are in the text not in the reference section.

Just wish there was an explanation somewhere.

Kharazyr (talk) 18:21, 16 January 2012 (UTC)

Incorrectnes in the Termination Rule

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)

Do you have a reference we can cite? - I guess you are right, anyway. In particular, if D is the set of nonnegative integers, and t is an 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 eventually found a reference: John C. Reynolds (2009). Theory of Programming Languages. Cambridge University Press.; Sect.3.4, p.64: P ∧ B ⇒ 0≤t,           [P ∧ B ∧ t=z] S [P ∧ t<z]/[P] while B do S done [P ∧ ¬B] when z is an integer ghost variable that doesn't occur free in P, B, S, or t, and t is an integer expression. - Jochen Burghardt (talk) 14:51, 3 January 2014 (UTC)

Replacement of free variables

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 }

You should observe that the version with the replacements done is the precondition, while the unreplaced version is the postcondition. So the converse of your above statement holds: if the postcondition were { 0 ≤ x ∧ x ≤ 9 } and the command x := y * y then there would only be one valid precondition, since every(I agree) instance of the free variable has to be replaced. - Jochen Burghardt (talk) 21:51, 14 April 2015 (UTC)

External links modified

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:

• Added archive https://web.archive.org/web/20071117054808/http://www.key-project.org/download/hoare/ to http://www.key-project.org/download/hoare/

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: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 16:27, 5 November 2017 (UTC)