Hoare triple: Loop invariant and correctness

Question

The following Hoare triple in which variable a is an array of integers, and len, max, i, n, j and m are integer-valued variables. Provide a loop invariant (using predicate logic) suitable for proving partial correctness of the Hoare triple. Explain in words why it is a loop invariant and why it is sufficient to prove partial correctness.

$$\begin{align*} &\{0 < len \} \\ &i = 0; \\ &n = 1; \\ &j = 0; \\ &m = 1; \\ &\textbf{while}\;(i+n < len)\;\{ \\ &\quad\textbf{if}\;(a[(i+n)]-a[(i+n-1)] ≤max)\;\{ \\ &\quad\quad n = n+1; \\ &\quad\quad \textbf{if} (m<n)\;\{ \\ &\quad\quad\quad j = i; \\ &\quad\quad\quad m = n; \\ &\quad\quad \}\;\textbf{else}\;\{skip\} \\ &\quad\ \}\;\textbf{else}\;\{ \\ &\quad\quad\quad i=i+n; \\ &\quad\quad\quad n=1; \\ &\quad\ \} \\ &\ \} \\ &\;\{0≤j∧1≤m∧(j+m)≤len∧ \\ &\quad\quad (∀ k : Z · ((j < k ∧ k < j+m) ⇒ (a[k] − a[(k−1)] ≤ max )))\} \end{align*}$$

I tried to use loop rule and get the invariant I by the third premise:

$$\{I \land \lnot b\} \; [] \; S \; \{Q\}$$

b is len ≤ i+n, but postcondition Q is too complex. Then I try to create two table to find rule, one table predicate a[(i+n)]−a[(i+n−1)]≤max, and predicate len = 6, then I get the program will terminate at fifth loop, and another table predicate a[(i+n)]−a[(i+n−1)]>max also len =6, I get the same answer that terminates at fifth loop. In addition, I tried one time ≤max and one time >max, then I get the same answer. So here I find a part of invariant which is loop times = len - 1. From above is what I did, but I have no idea about how to go next step.

Answer 1

I believe the loop invariant is the same as the postcondition, except with j and m swapped with i and n, respectively. That statement can be proven true at the start and end of each loop. This is true partially by virtue of the fact that the final implication is trivially true when n = 1 (as in the outer else condition), because no k value is in the range.

The fact that j and m are only ever assigned from i and n while the invariant is true, and the postcondition is true prior to the loop, implies that the postcondition holds.

Another key observation is that i+n < len implies i+n+1 ≤ len, so the proposed invariant holds true, even after the loop condition fails.

I hope that helps.