View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000365 | Frama-C | Documentation > manuals | public | 2010-01-04 17:52 | 2016-06-21 14:20 | ||||
Reporter | dwheeler | ||||||||
Assigned To | cmarche | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Beryllium-20090902 | ||||||||
Target Version | Fixed in Version | Frama-C Carbon-20101201-beta1 | |||||||
Summary | 0000365: Jessie tutorial binary_search examples fail with Why 2.23 - loop variant must be added | ||||||||
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) | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2010-01-04 17:52 | dwheeler | New Issue | |
2010-01-05 08:40 | signoles | Status | new => assigned |
2010-01-05 08:40 | signoles | Assigned To | => cmarche |
2010-01-05 08:41 | signoles | Relationship added | related to 0000079 |
2010-02-01 13:01 | cmarche | Status | assigned => resolved |
2010-02-01 13:01 | cmarche | Resolution | open => fixed |
2010-02-01 13:01 | cmarche | Additional Information Updated | |
2010-12-10 15:45 | signoles | Fixed in Version | => Frama-C Carbon-20101201-beta1 |
2010-12-17 19:37 | signoles | Status | resolved => closed |
2016-06-21 14:11 | signoles | Category | Documentation => Documentation > ACSL |
2016-06-21 14:20 | signoles | Category | Documentation > ACSL => Documentation > manuals |