correctnesshoare-logic

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


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:

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


Solution

  • 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:

    So the original Hoare triple holds.