~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to tests/jessie/binary_search.c

• browse files at revision 1
• compare with another revision
• download diff
• download tarball
• view history from revision 1

Show diffs side-by-side

added

removed

tests/jessie/binary_search.c

 

1

 

 

2

/*@ lemma mean_1 : \forall int x, int y; x <= y ==> x <= (x+y)/2 <= y; */

 

3

 

 

4

/*@ requires

 

5

  @   n >= 0 && \valid_range(t,0,n-1) &&

 

6

  @   \forall int k1, int k2; 0 <= k1 <= k2 <= n-1 ==> t[k1] <= t[k2];

 

7

  @ ensures

 

8

  @   (\result >= 0 && t[\result] == v) ||

 

9

  @   (\result == -1 && \forall int k; 0 <= k < n ==> t[k] != v);

 

10

  @*/

 

11

int binary_search(int* t, int n, int v) {

 

12

  int l = 0, u = n-1, p = -1;

 

13

  /*@ loop invariant

 

14

    @   0 <= l && u <= n-1 && -1 <= p <= n-1

 

15

    @   && (p == -1 ==> \forall int k; 0 <= k < n ==> t[k] == v ==> l <= k <= u)

 

16

    @   && (p >= 0 ==> t[p]==v);

 

17

    @ loop variant u-l;

 

18

    @*/

 

19

  while (l <= u ) {

 

20

    int m = (l + u) / 2;

 

21

    //@ assert l <= m <= u;

 

22

    if (t[m] < v)

 

23

      l = m + 1;

 

24

    else if (t[m] > v)

 

25

      u = m - 1;

 

26

    else {

 

27

      p = m; break;

 

28

    }

 

29

  }

 

30

  return p;

 

31

}

 

32

 

 

33

/* 

 

34

Local Variables:

 

35

compile-command: "PPCHOME=../.. LC_ALL=C make binary_search"

 

36

End:

 

37

*/

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1