semantics - How do I infer the weakest precondition when a loop invariant is given? - Stack Overflow

admin管理员组

文章数量:1291002

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?

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?

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

Share Improve this question Follow asked Feb 13 at 21:54 desert_rangerdesert_ranger 1,74333 gold badges2020 silver badges4343 bronze badges 4

• 1 Questions like these seem more appropriate for Computer Science than Stack Overflow. – 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 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 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 Commented Feb 14 at 13:27

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 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.

本文标签： semanticsHow do I infer the weakest precondition when a loop invariant is givenStack Overflow