请求推导指定程序的循环不变式并说明推导方法

Hey there! I totally get how loop invariants can feel elusive at first—like trying to spot a pattern that's just out of reach. Let's walk through this program step by step, and I'll show you exactly how to derive the invariant, plus the general approach you can use for other loops.

A loop invariant is a logical condition that stays true through every step of the loop. To be valid, it needs to satisfy three key rules:

• Initialization: It holds true right before the loop starts executing.
• Maintenance: If it's true before one iteration of the loop, it's still true after that iteration finishes.
• Termination: When the loop stops running, the invariant plus the loop's termination condition will directly prove the postcondition we want.

Your program's postcondition is:

∀j.(0 ≤ j < n − 1 → b[j] = a[j + 1])

In plain English: For every index j from 0 up to (but not including) n-1, the value of b[j] equals a[j+1]. The loop works by iterating i from 0 to n-2 (since the loop condition is i < n-1), copying a[i+1] to b[i] each time, then incrementing i.

The invariant should describe a "partial" version of this postcondition—what we've accomplished so far at any point during the loop.

Let's think about the state mid-loop: when the loop variable is at value i, we've already copied the values for all indices j from 0 to i-1. We also need to track the valid range of i (since it starts at 0 and stops at n-1), and keep the initial condition n ≥0 (since that never changes).

Putting this all together, our candidate invariant P is:

n ≥ 0 ∧ 0 ≤ i ≤ n-1 ∧ ∀j.(0 ≤ j < i → b[j] = a[j+1])

Now we need to make sure this invariant checks all three boxes:

1. Initialization (Holds Before the Loop Starts) #

The precondition is {n ≥ 0 ∧ i = 0}. Plugging into our invariant:

• n ≥0 is given, so that's true.
• 0 ≤ 0 ≤ n-1: If n=0, n-1=-1, but the loop condition i <n-1 becomes 0 < -1 (false), so the loop never runs—this edge case is still valid. For n≥1, n-1≥0, so 0 ≤0 ≤n-1 holds.
• ∀j.(0 ≤j <0 → b[j]=a[j+1]): The range 0 ≤j <0 is empty, so this universal statement is automatically true (there are no j's to violate it).

All parts hold, so initialization passes.

2. Maintenance (Holds After Each Iteration) #

Suppose P is true before an iteration, and the loop condition i <n-1 is true (so we enter the loop). Let's run the loop body:

1. b[i] := a[i+1]: We set b[i] to match a[i+1].
2. i := i+1: We increment i to a new value i' = i+1.

Now we need to prove P holds for i':

• n ≥0 is still true (n doesn't change).
• 0 ≤i' ≤n-1: Since i <n-1, i' =i+1 ≤n-1 (because i ≤n-2). And since i≥0, i'≥1≥0. So this holds.
• ∀j.(0 ≤j <i' →b[j]=a[j+1]): i'=i+1, so j ranges from 0 to i. For j <i, the invariant already guaranteed b[j]=a[j+1]. For j=i, we just set b[i]=a[i+1] in the loop body. So all j's in the range satisfy the condition.

Maintenance checks out.

3. Termination (Implies the Postcondition) #

When the loop stops, the loop condition i <n-1 is false—so i ≥n-1. From our invariant P, we know 0 ≤i ≤n-1. Combining these two, we get i =n-1.

Now substitute i=n-1 into the invariant's universal statement:

∀j.(0 ≤j <n-1 →b[j]=a[j+1])

That's exactly the postcondition we needed to prove! Perfect—termination passes.

To recap, here's how you can tackle any loop invariant problem:

• Start with the end goal: The invariant is almost always a partial version of the postcondition, describing what's been completed so far.
• Track the loop variable: Include constraints on the loop counter (like 0 ≤i ≤n-1 here) to define the boundary between completed and uncompleted work.
• Check the three rules: If your candidate invariant fails any of initialization/maintenance/termination, tweak it (e.g., adjust the range of j, add a missing constraint).
• Don't forget edge cases: Make sure your invariant holds even when the loop runs 0 times (like n=0 here).

内容的提问来源于stack exchange，提问作者the_martian