Menu
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?
591
A Hoare triple has three parts, a precondition P, a program statement or series of statements S, and a postcondition Q. It's usually written in the form. {P} S {Q} The meaning is "if P is true before S is executed, and if the execution of S terminates, then Q is true afterwards".
{{X = 0}} X ::= X + 1 {{X = 1}} is a valid Hoare triple, stating that command X ::= X + 1 would transform a state in which X = 0 to a state in which X = 1.
The strongest postcondition possible is x = 10; this is the most useful postcondition. Formally, if {P} S {Q} and for all Q such that {P} S {Q}, Q ⇒ Q, then Q is the strongest postcondition of S with respect to P.
If precondition P is false, then the Hoare-triple guarantees nothing about execution, so execution of S can do anything! It can get into an infinite loop; it can stop immediately, with no guarantees about what state it is in; it can abort in some fashion, perhaps by dividing by 0.
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
x := y given postcondition { x = y } is { y = y }, and{ 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.
81
{ 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}.
33
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
