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

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

Relationships

related to

0000079

assigned

virgile

Better support of //@ style

Notes
There are no notes attached to this issue.

Issue History
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