5

I am not sure that

{ true } x := y { x = y }

is a valid Hoare triple.

I am not sure one is allowed to reference a variable (in this case, y), without explicitly defining it first either in the triple program body or in the pre-condition.

{ y=1 } x := y { x = y } //valid

{true} y := 1; x := y { x = y } //valid

How is it?

aioobe
  • 413,195
  • 112
  • 811
  • 826
devoured elysium
  • 101,373
  • 131
  • 340
  • 557
  • 2
    cstheory aims at research level discussions. this is a basic CS question. – devoured elysium Oct 02 '11 at 20:28
  • Ok, looks like SO fails at basic CS then :-) (I'd never heard of Hoare logic before) – Mat Oct 02 '11 at 20:33
  • http://en.wikipedia.org/wiki/Hoare_logic – devoured elysium Oct 02 '11 at 20:35
  • Yeah, found that before suggesting cstheory. I'm not sure your first statement/triple is "useful", since it's just a special case of the assignment axiom with `P` = `true`. I'm not sure a pre-condition that doesn't specify anything about the variables can be "useful". – Mat Oct 02 '11 at 20:46
  • 1
    Unfortunately, all the explanations of Hoare logic (including the one on Wikipedia) have been written by grammatically challenged foreigners. It's that way mostly in formal logic. I'm still waiting for a text written for people who are fluent in English. – Roger F. Gay Oct 02 '11 at 21:02
  • @Mat: I am not asking about its usefulness, but whether or not it is a valid triple. – devoured elysium Oct 04 '11 at 07:31
  • @devouredelysium: what's the point of wondering whether or not something that can't add value is valid? – Mat Oct 04 '11 at 07:41
  • 3
    That's the same as asking what's the point of knowing if x = x; in C is valid or not. – devoured elysium Oct 04 '11 at 08:28
  • I have no idea why you haven't accepted the answer below yet. It answers your question but you claim it doesn't. Either you need to clarify your question or ... be that as it may, here's the link to the theoretical cs Q&A forum: http://cstheory.stackexchange.com/ – Roger F. Gay Oct 06 '11 at 13:31

3 Answers3

6

I am not sure that

{ true } x := y { x = y }

is a valid Hoare triple.

The triple should be read as follows:

      "Regardless of starting state, after executing x:=y x equals y."

and it does hold. The formal argument for why it holds is that

  1. the weakest precondition of x := y given postcondition { x = y } is { y = y }, and
  2. { true } implies { y = y }.

However, I completely understand why you feel uneasy about this triple, and you're worried for a good reason!

The triple is badly formulated because the pre- and post condition do not provide a useful specification. Why? Because (as you've discovered) x := 0; y := 0 also satisfies the spec, since x = y holds after execution.

Clearly, x := 0; y := 0 is not a very useful implementation and the reason why it still satisfies the specification, is (according to me) due to a specification bug.

How to fix this:

The "correct" way of expressing the specification is to make sure the specification is self contained by using some meta variables that the program can't possible access (x₀ and y₀ in this case):

{ x=x₀ ∧ y=y₀ } x := y { x=y₀ ∧ y=y₀ }

Here x := 0; y := 0 no longer satisfies the post condition.

aioobe
  • 413,195
  • 112
  • 811
  • 826
1

{ true } x := y { x = y } is a valid Hoare triple. The reason is as follows:

x := y is an assignment, therefore, replace that in the precondition.
The precondition stands as {y=y}, which implies {true}.

In other words, {y=y} => {true}.

Anne
  • 26,765
  • 9
  • 65
  • 71
Swarnendu Biswas
  • 11
  • 1
-2

* If x:=y, then Q. Q.E.D. _*

Roger F. Gay
  • 1,830
  • 2
  • 20
  • 25
  • 1
    Sure. An apple is an apple. A pear is a pear. A green turtle is a green turtle. If (x:=y) then x=y. So, if you've got two green turtles, then they're both green turtles. Same with two big green turtles, etc. – Roger F. Gay Oct 02 '11 at 21:45
  • Put another way: A=A if A:=A. – Roger F. Gay Oct 02 '11 at 21:48
  • Perhaps you need to add explanation to your question. Are you asking in the context of a specific language implementation or in a specific concrete implementation context? That would make the question something other than what's stated, IMO. Generally speaking, a statement leads to itself as a conclusion. – Roger F. Gay Oct 03 '11 at 07:58
  • Actually, it doesn't so much "lead to itself" as it's already there. – Roger F. Gay Oct 03 '11 at 09:08
  • Also note that what's true generally (x=y) is also true specifically (when y=1). It's just a specific case with y=1. It's not needed to validate x=y when x:=y. – Roger F. Gay Oct 03 '11 at 09:31
  • 1
    This was tagged as Hoare Logic. This is not some "specific implementation" or any programming language. – devoured elysium Oct 03 '11 at 12:10
  • 1
    It doesn't answer in any way to what was asked in the OP. – devoured elysium Oct 03 '11 at 15:53
  • Then you need to explain your OP (including what "OP" stands for). It's perfectly clear that men are men, women are women, and small furry creatures from Alpha Centauri are small furry creatures from Alpha Centauri. The logic is valid whether or not small furry creatures from Alpha Centauri exist. – Roger F. Gay Oct 03 '11 at 18:13