How to find the loop invariant and prove correctness?

Question

int i, temp; 
a is an array of integers [1...100] 

i = 1; 

while i < 100 
    if a[i] > a[i+1] 
        temp = a[i]
        a[i] = a[i+1]
        a[i+1] = temp 
    i = i+1

I'm having trouble understanding how to find loop invariants and writing a formal statement for them. So a loop invariant is just a condition that is true immediately before and after each iteration of a loop. It looks like the code is doing a swap: if the following element is greater in the array than the current one, switch places. I mean from the definition of a loop invariant, it really sounds like it's i < 100 because that must be true for the loop to run, but I don't really understand. Would greatly appreciate some clarification.

Answer 1

Going by your definition, I can see two loop invariant conditions:

1. i < 100
2. a[i] = greater than a[j] for all j < i, where i is the loop variable.

This is in fact one outer loop iteration of bubble sort. At the end of this loop, the highest value in the array bubbles to the top (a[100]) .