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

Question

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?

Questions like these seem more appropriate for Computer Science than Stack Overflow. — Barmar
– Barmar, Commented Feb 13 at 22:03
I agree. The issue is that the C.S StackExchange has a much smaller population as compared to S.O. — desert_ranger
– desert_ranger, Commented Feb 13 at 22:10
Perhaps true, but the vast majority of the population here are useless in answering these questions. I've been programming for 45 years, I have no idea what Hoare logic is, and I've never done any formal verification. I know about loop invarirants and pre/post-conditions, but rarely think about them much. — Barmar
– Barmar, Commented Feb 13 at 22:51
Your simplified WP for that if is wrong; it says x can't be 0, but x ends up as 1 if you start the if with x=0, which satisfies your postcondition. In fact, it says x can't be 1 either, but x ends up 0 if you start with x=1, which also satisfies your postcondition. — Scott Hunter
– Scott Hunter, Commented Feb 14 at 13:27

Scott Hunter · Accepted Answer · 2025-02-14 13:29:05Z

1

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.

edited Feb 14 at 13:29

answered Feb 14 at 13:21

Scott Hunter

50k12 gold badges65 silver badges107 bronze badges

Sign up to request clarification or add additional context in comments.

Comments

Rafael Martinez · Accepted Answer · 2025-06-18 11:36:54Z

There are some failures in your exposure. Let me help you.

wp(P, S) formalizes "the weakest precondition give P as post condition an S as code".

Hence, in your case, let's proceed in a step-by-step way....

A)

wp(P, if B then S1 S2) ::= (b -> wp(P,S1) ) and ( not b -> wp(P, S2)) , that is...

wp(x>=0, if x > 0: x = x - 1 else: x = x + 1) = ... ** I omitted steps to justify wp(P,x=e)... = (x> 0 -> x-1>= 0) and ( x <=0 -> x >= -1) = true and ( x <=0 -> x >= -1) = x >= -1

that is, program before if can start with -1,0,1,2,3,100, and it will fit x>=0.

B) Now, two observations:

your program, as it is, can not terminate... it is and endless loop as quota never decreases (informally, you don't increase i).
Eventhough, we can still partial correctness, that is: if the program terminates it will fit the desired property x >= 0 .
The weakest precondition for a given post condition and a loop , i.e. wp(P, while B do S) is not decidable**. We call it invariant (I).** You have to guess, based on your "intuition". Let's propose (I: x>=0) for your P: x>=0 which fits the property the desired properties for I:
it implies post. i.e: I and not B -> P , since (x>=0 and i >= 10 )-> x>=0 (trivial)
it is indeed invariant: I and B -> wp(x>=0, if x > 0: x = x - 1 else: x = x + 1) . As calculated in step A (wp:x>=-1) : x>=0 and i >=1 -> x>=-1 (you see why?)

C) Now, we are ready to finally infer the weakest precondition for the program. Mind that with (basic) Hoare logic you cannot use I/O statements (user_input) (informally, they might invalidate the invariant at the will of user, (entering -2 will make it fail). Hence call that value N as constant.

wp(x>=0, S1;S2) = wp( wp(x>=0,S2),S1) = wp ( N>=0, i=0) = N>=0

This is your answer for the whole program : N>=0

Below you will find your (endless) program annotated.

# { N>=0} weakest precondition for the whole program. 
i = 0
# {N>=0}
x = N ; # user_input, you cannot use I/O !!!
# I : x >= 0
while i < 10:   # B 
    # I and B : {x>=0 and i < 10} 
    # { x >= -1 }  
    if x > 0:
        # { x >= 1 } 
        x = x - 1
    else:
        # { x >= -1 }
        x = x + 1
    # { x >= 0 }
# I and not B : { x>= 0 and i >= 10 }
# Postcondition: { x >= 0 }

Sorry, your endless loop was formulated right in stackoverflow.com/questions/79437554/…. I hope my contribution is useful your "meta" question there

Collectives™ on Stack Overflow

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

2 Answers 2

Comments

1 Comment

Your Answer

Linked

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

Comments

1 Comment

Your Answer

Sign up or log in

Post as a guest

Linked

Related