I am trying to write a proof using a loop invariant for an algorithm that I wrot
ID: 3881449 • Letter: I
Question
I am trying to write a proof using a loop invariant for an algorithm that I wrote, where A is the array and v is the value being searched for:
bSearch(A, v) {
return binarySearch(A, 0, length(A)-1, v)
}
binarySearch(A, l, r, v) {
if l >= r:
return -1
p = l+(r-1)/2
if A[p] == v:
return p
if A[p] < v
return binarySearch(A, p-1, r, v)
else return binarySearch(A, l, p-1, v)
}
I am having trouble determining what the loop invariant is. I understand that the loop comes from the recursive nature of the algorithm, and I believe the loop invariant has something to do with the value of p, and the sequence of if statements. I also know that p is the value being returned, and that it is the index where v is found. Any insight on the specifics of the identity loop invariant/ what line it is on would be awesome. Thank you!
Explanation / Answer
Loop invariant:
- holds true immediately before and immediately after a loop iteration. (may or may not hold during the iteration)
In this case, the recursive procedure is used to iterate through the elements. In this case, it is better be called recursive invariant and not loop invariant.
The premise is same as before: "must hold true before and after each recursive call".
One recursive invariant for the given given procedure can be the following:
"If the element v exists in array A, then it exists between index position l and r where l < r"
Related Questions
drjack9650@gmail.com
Navigate
Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.