examples/micro-c/loops.c

   1
   2 #include <stdio.h>
   3
   4 void loop1(int b)
   5 //@ requires b > 0;
   6 {
   7   while (--b) {
   8     //@ invariant b > 0;
   9     //@ variant b;
  10     ;
  11   }
  12   //@ assert b == 0;
  13 }
  14
  15 void loop2(int b)
  16 //@ requires b >= 0;
  17 {
  18   while (b) {
  19     //@ invariant b >= 0;
  20     //@ variant b;
  21     b--;
  22   }
  23   //@ assert b == 0;
  24 }