0
$\begingroup$

I've been assigned to find the loop invariant for the following code:

i=0;
j=n-1;
while(i < n/2){
    l = A[i];
    r = A[j];
    A[j] = l;
    A[i] = r;
    j = j-1;
    i = i+1;
}

I understand the code function (reverses array), the guard (i < n/2), and I can find different invariants (e.g. i+j = n-1), but I'm stuck finding anything useful that relates the precondition:

A[0], A[1] ... A[n-2], A[n-1]

to the postcondition:

A[n-1], A[n-2] ... A[1], A[0]

Can anyone help with this problem, or even generally how to find useful invariants for loops that operate on arrays?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ Those aren't preconditions/postconditions. What reading and study have you done? What do you understand about loop invariants, and what progress have you made? Can you write down any proposition that will be true on every iteration of the loop, anything at all? $\endgroup$ Commented Jun 2, 2022 at 4:24

1 Answer 1

Reset to default
2
$\begingroup$

The invariant will express that we have performed a partial reversal, i.e. the array zones A[0..i[ and A[n-i..n[ have been swapped the intended way, while the middle is unchanged.

So, if you denote the initial content of the array as Z, the invariant is like

Forall k: k < i => A[k] = Z[n-k] and n/2 > k ≥ i => A[k] = Z[k]

(Caution: off-by-one errors are possible, I didn't check.)

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.