## Jessie tutorial binary_search examples fail with Why 2.23 - loop variant must be added

ID0000365:
**This issue was created automatically from Mantis Issue 365. Further discussion may take place here.**

Id |
Project |
Category |
View |
Due Date |
Updated |
---|---|---|---|---|---|

ID0000365 | Frama-C | Documentation > manuals | public | 2010-01-04 | 2016-06-21 |

Reporter |
dwheeler | Assigned To |
cmarche | Resolution |
fixed |

Priority |
normal | Severity |
minor | Reproducibility |
always |

Platform |
- | OS |
- | OS Version |
- |

Product Version |
Frama-C Beryllium-20090902 | Target Version |
- | Fixed in Version |
Frama-C Carbon-20101201-beta1 |

### Description :

The Jessie tutorial in: http://frama-c.cea.fr/jessie_tutorial_index.html sections 2.1 and 2.2 include binary_search examples. If "Why" is upgraded to Why 2.23, these no longer work, because there is no loop variant provided.

The single loop invariant must be changed to be: /*@ loop invariant 0 <= l && u <= n-1; loop variant u-l; */

In addition, explain loop variants, since they are absolutely necessary to use Why 2.23.

Also, please note in the documentation that this will NOT work: //@ loop invariant 0 <= l && u <= n-1; //@ loop variant u-l; Basically, make it clear that you're not allowed to have "//@" in succession, especially since doing this produces a mysterious and misleading error message. See bug 79.

The example of 2.2 should end up looking like this (the lemma is optional):

/*@ lemma mean: \forall integer x, y; x <= y ==> x <= (x+y)/2 <= y; /
//@ requires n >= 0 && \valid_range(t,0,n-1);
int binary_search(int t, int n, int v) {
int l = 0, u = n-1, p = -1;
/*@ loop invariant 0 <= l && u <= n-1;
@ loop variant u-l; */
while (l <= u ) {
int m = l + (u - l) / 2; // NOTE this is changed for bounded calculation
if (t[m] < v)
l = m + 1;
else if (t[m] > v)
u = m - 1;
else {
p = m; break;
}
}
return p;
}

### Additional Information :

Fixed in Frama-C SVN (doc/jessie)