Is {true} x := y { x = y } a valid Hoare triple?

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 ex开发者_StackOverflow中文版plicitly 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?

---

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.

---

{ 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}.

---

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