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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.