Validity of Hoare triple with unknown variable in program and post-condition?

Question

I'm unsure about the value of x in this Hoare triple: { a = 0 } while (x > a) do (x := x − 1) { x = 0 }.

I have 2 potential ideas for how to prove whether this Hoare triple is valid or not:

• Assuming x is 0, the Hoare triple is valid, or
• Assuming x is any arbitrary value, we break it down into cases and conclude that the Hoare triple is not valid for all values of x

Are either of the above approaches valid, or is there another approach I should take?

Answer 1

So you have

{a = 0}
while (x > a)
    x := x - 1
{x = 0}

Let's try the loop invariant x ≥ a & a = 0 and let's abbreviate it with I. When we annotate the program, we get:

{a = 0}
{I}              # Loop invariant should be true before the loop
while (x > a)
    {I & x > a}  # Loop invariant + condition holds
    x := x - 1
    {I}          # Loop invariant should be true after each iteration
{I & x ≤ a}      # Loop invariant + negation of loop condition
{x = 0}

Now we need to apply the weakest precondition to x := x - 1:

{a = 0}
{I}
while (x > a)
    {I & x > a}
    {x - 1 ≥ a & a = 0}  # I[x-1/x]
    x := x - 1
    {I}
{I & x ≤ a}
{x = 0}

We end up with the following proof obligations:

• (a = 0) ⇒ (x ≥ a & a = 0) holds, since x ∈ ℕ
• (x ≥ a & a = 0) ⇒ (x - 1 > a & a = 0), holds. Proof trivial.
• (x ≥ a & a = 0 & x ≤ a) ⇒ (x = 0) holds. Proof trivial.

So the original Hoare triple holds.