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] < 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 :

Do You reckon this is correct?

Solution

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

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.