Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #472

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)

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking