CODEWITHSUNDEEP
semanticsformal-verificationloop-invariantpost-conditionshoare-logic
desert_ranger
desert_ranger

Reputation: 1743

How do I infer the weakest precondition when a loop invariant is given?

I previously asked this question on StackOverflow about using loop invariants to catch a bug in my program. Now, I want to take the next step and understand how to compute the weakest precondition when a loop invariant is provided.

Background: For a simple if-statement, I understand how to compute the weakest precondition. Consider the following code:

if x > 0:
    x = x - 1
else:
    x = x + 1
# Postcondition: { x >= 0 }

To ensure that the postcondition x >= 0 holds after execution, I compute the weakest precondition as:

(x>0/\x>=1)\/(x<0/\(x+1)>=0)

which simplifies to:

(x>1)∨(−1<x<0)

However, I don’t know how to compute the weakest precondition when there is a loop and a given loop invariant.

My Question: Consider the following loop:

i = 0
x = user_input
while i < 10:
    if x > 0:
        x = x - 1
    else:
        x = x + 1
# Postcondition: { x >= 0 }

For some loop invariant I provided and proved (x>=0), how do I formally infer the weakest precondition for the entire program using my postcondition and invariant with backward reasoning?

Upvotes: 0

Views: 49

Answers (1)

Scott Hunter
Scott Hunter

Reputation: 49896

Filling in the assertions between statements:

i = 0
x = user_input
{ x >= 0 }
while i < 10:
    { x >= 0 }
    if x > 0:
        { x > 0 }
        { x >= 1 }
        { x-1 >= 0 }
        x = x - 1
        { x >= 0 }
    else:
        { x <= 0 && x >= 0}
        { x = 0 }
        { x+1 >= 0} {x >= -1 } 
        x = x + 1
        { x >= 0 }
# Postcondition: { x >= 0 }

Since nothing happens between reading x & the loop, the loop's invariant would be your weakest precondition.

Note: the whole point of having a loop invariant is that you can use the same reasoning as you would for more "static" code.

Upvotes: 1

Related Questions