semantics - How do I use a loop invariant to catch a bug in my program? - Stack Overflow

admin管理员组

文章数量:1291061

I’m learning about weakest preconditions, loop invariants, and verifying program correctness (e.g., with an SMT solver). From the slides here in slide 11, I see how placing a loop invariant can help me prove (or disprove) that my program meets its postcondition.

I created the following minimal program to test this idea. The program traverses an integer number line for 10 iterations, and I want to ensure it never goes below zero. I placed x >= 0 as my loop invariant and postcondition. However, I deliberately introduced a bug:

i = 0
x = user_input  # Assume we require x >= 0 initially.
while i < 10:
    if x >= 0:
        # Faulty edge-case: instead of protecting x, we subtract 1, which will make it negative.
        x = x - 1  
    else:
        # Normal behavior: increment x to stay safely above zero.
        x = x + 1
    i += 1
    # loop invariant: { x >= 0 }
# Postcondition: x >= 0

If x starts at 0, the predicate x >= 0 evaluates to true, so the program executes x = x - 1, making x negative. This clearly violates the intended invariant x >= 0.

My questions:

How exactly would the loop invariant x >= 0 be used to identify this bug in a formal verification or SMT-based approach? I understand that the invariant must hold at the start (and end) of each iteration, but I’m unsure how that translates into a proof or a verification condition that flags the code as incorrect.

Meta Question I know we often derive a precondition using backward reasoning to ensure the loop invariant holds initially, but I’m not fully clear on how to formally derive it (e.g., x >= 0 initially) with the loop invariant and the postcondition. I suppose that would be needed to answer my main question.

I hope my question is clear. I’d appreciate any pointers on how to show, via loop invariants (and possibly weakest precondition reasoning and a SMT), that this program is not correct—specifically, that the code fails the invariant if x starts at 0.

I’m learning about weakest preconditions, loop invariants, and verifying program correctness (e.g., with an SMT solver). From the slides here in slide 11, I see how placing a loop invariant can help me prove (or disprove) that my program meets its postcondition.

I created the following minimal program to test this idea. The program traverses an integer number line for 10 iterations, and I want to ensure it never goes below zero. I placed x >= 0 as my loop invariant and postcondition. However, I deliberately introduced a bug:

i = 0
x = user_input  # Assume we require x >= 0 initially.
while i < 10:
    if x >= 0:
        # Faulty edge-case: instead of protecting x, we subtract 1, which will make it negative.
        x = x - 1  
    else:
        # Normal behavior: increment x to stay safely above zero.
        x = x + 1
    i += 1
    # loop invariant: { x >= 0 }
# Postcondition: x >= 0

If x starts at 0, the predicate x >= 0 evaluates to true, so the program executes x = x - 1, making x negative. This clearly violates the intended invariant x >= 0.

My questions:

How exactly would the loop invariant x >= 0 be used to identify this bug in a formal verification or SMT-based approach? I understand that the invariant must hold at the start (and end) of each iteration, but I’m unsure how that translates into a proof or a verification condition that flags the code as incorrect.

Meta Question I know we often derive a precondition using backward reasoning to ensure the loop invariant holds initially, but I’m not fully clear on how to formally derive it (e.g., x >= 0 initially) with the loop invariant and the postcondition. I suppose that would be needed to answer my main question.

I hope my question is clear. I’d appreciate any pointers on how to show, via loop invariants (and possibly weakest precondition reasoning and a SMT), that this program is not correct—specifically, that the code fails the invariant if x starts at 0.

• semantics
• formal-verification
• post-conditions
• hoare-logic

Share Improve this question Follow edited Feb 13 at 20:31 desert_ranger asked Feb 13 at 19:41 desert_rangerdesert_ranger 1,74333 gold badges2020 silver badges4343 bronze badges 1

• I have elaborated on my meta question over here - stackoverflow/questions/79437806/… – desert_ranger Commented Feb 13 at 21:55

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 1

You need to be able to prove that {x >= 0} x = x-1 {x >= 0} is true, which you can't (x starting as 0 is the counterexample).

I'm not clear what your meta-question is.

本文标签： semanticsHow do I use a loop invariant to catch a bug in my programStack Overflow