examples/micro-c/triangular.c

   1
   2 #include <stdio.h>
   3
   4 // la somme des n premiers entiers
   5
   6 int triangular(int n)
   7 //@ requires n >= 0;
   8 //@ ensures  result == n * (n + 1) / 2;
   9 {
  10   int s = 0;
  11   for (int k = 0; k <= n; k++) {
  12     //@ invariant k <= n + 1;
  13     //@ invariant s == (k - 1) * k / 2;
  14     //@ variant   n - k;
  15     s += k;
  16   }
  17   return s;
  18 }
  19
  20 int triangular2(int n)
  21 /*@ requires n >= 0;
  22   @ ensures  result == n * (n + 1) / 2;
  23   @ variant  n; */
  24 {
  25   if (n == 0) return 0;
  26   return n + triangular2(n - 1);
  27 }
  28
  29 int main() {
  30   printf("somme 1 + .. + 100 = %d\n", triangular(100));
  31   printf("somme 1 + .. + 100 = %d\n", triangular2(100));
  32   return 0;
  33 }