Talk:Hoare logic

From Wikipedia, the free encyclopedia

This article is part of a WikiProject to improve Wikipedia's articles related to Computer science. For guidelines see WikiProject Computer science and Wikipedia:Contributing FAQ.

[edit] 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)

[edit] 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)

[edit] 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? —The preceding unsigned comment was 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)