Binary chop: if list[middle] == key case

I'm revising algorithms for my exams and I was trying to solve this exercise but I couldn't come up with a solution.

This is the pseudo-code.

1. int search (int [] a, int x) {
2. // Pre: ∃i:Nat (0≤i<a.length ∧ a[i]=x) ∧ a is in ascending order
3. // Post: 0≤ r≤ a.length ∧
4. // ∀i:int.(0 ≤ i < r → a[i] <开发者_如何学Go x) ∧ a[r]=x
5. int left, middle; int right = a.length;
6. if (a[0]>=x) return 0; else left=0; //a[left]<x (a)
7. while ((right-left>1){ (b)
8. // invariant: (I1) 0≤ left < right ≤ a.length ∧
9. // (I2) ∀i:int(0 ≤ i ≤ left → a[i] < x) ∧
10. // (I3) ∀i:int(right ≤ i < a.length → a[i] > x)
11. // (note: a[i]>x not a[i]≥x)
12. // Variant: right-left-1
13. middle = (left+right) / 2; // left < middle < right (*)
14. if ( a[middle]== x) return middle;
15. else {if a[middle)<x) left = middle ;
16. else right=middle;} (c)
17. }
18. } // left+1=right } (d)

So, the code as it is now doesn't satisfy the post condition because for certain inputs (e.g. x = 1 and a={0,1,1,1,1}) the value returned by line 14 doesn't satisfy the post-condition on line 4. The exercise is asking to : "Replace "return middle;" on line 14. by a while loop and return code so that it satisfies the postcondition. Include variant and invariant strong enough to imply the postcondition on return. Hint: Make sure you include to state what doesn't change."

I have not been able to find a solution. Can anyone help me?

Thanks in advance, VJ

EDIT: Ok, thank you both of you for your help.

while(middle > 0 && a[middle] == x){
middle--;

} return middle;

I chose the variant to be middle. And the invariant to be :

0x

Do You reckon this is correct?

---

When a[middle] = x we are sure we should return index middle or something before it, if there are the same values before middle.

So

if (a[middle]==x) {
    while (--middle>0 && a[middle]==x) {};
    return middle+1;
}

But that can be slow, for example when whole a contains the same values it has linear time complexity.

---

Ajuc has posted a solution using a loop, but as he said this can be slow.

A faster approach is to again use binary search on the left array. If it is not found return i, else return the result of this binary search. The complexity will remain the same (O(logn)).

Since this looks like homework I will let you figure out the rest by yourself :).