Talk:Hoare logic

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)

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)

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)