Is {truth} x: = y {x = y} a real Hoar triple?

Question

I'm not sure

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

valid Hoare triple .

I am not sure that it is allowed to refer to a variable (in this case, y ), without explicitly defining it first either in the triple body of the program or in the precondition.

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

Like this?

Answer 1

I'm not sure

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

- The actual troika of Hore.

The three should be read as follows:

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

and it is executed. The formal argument in favor of why it is executed is that

• the weakest condition x := y given postcondition { x = y } is { y = y } , and
• { true } implies { y = y } .

However, I fully understand why you feel awkward about this three, and you worry for a good reason!

The triple is poorly formulated, because the before and after condition does not provide a useful specification. What for? Because (as you discovered) x := 0; y := 0 x := 0; y := 0 also satisfies the specification since x = y is executed after execution.

Obviously, x := 0; y := 0 x := 0; y := 0 not a very useful implementation, and the reason it still satisfies the specification is (for me) due to a specification error.

How to fix it:

The “correct” way to express a specification is to make sure that the specification is autonomous using some meta variables that the program cannot access ( x₀ and y₀ in this case):

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

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

Answer 2

{ true } x := y { x = y } is a real Choir triple. The reason is this:

x := y is the destination, so replace this in the precondition.
The precondition is like {y=y} , which means {true} .

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

Answer 3

* If x: = y, then QQED _ *