# Hoare triple: Loop invariant and correctness

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

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.