File: Malcolm.c

package info (click to toggle)
why 2.13-2
  • links: PTS, VCS
  • area: main
  • in suites: lenny
  • size: 12,608 kB
  • ctags: 16,817
  • sloc: ml: 102,672; java: 7,173; ansic: 4,439; makefile: 1,409; sh: 585
file content (19 lines) | stat: -rw-r--r-- 290 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
 
/*@ logic int my_log(real s) */

/*@ ensures \result == 2 ^^ (53) */

double malcolm1() {
  double A;
  A=2;
  /*@ assert A==2 */

  /*@ invariant A== 2 ^^ my_log(A) && 
              1 <= my_log(A) <= 53
      variant (53-my_log(A)) */

  while (A != (A+1)) {
    A*=2;
  }
  return A;

}