0
$\begingroup$

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.

$\endgroup$

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.