bench/infer/while2.mlw

   1 module While2
   2
   3         use int.Int
   4         use ref.Ref
   5
   6         let b [@infer] [@bddinfer] (_:int) : int
   7         ensures { result = 0 }
   8         =
   9                 let i = ref 0 in
  10                 let j = ref 0 in
  11                 j := 0;
  12                 i := 1;
  13                 while !i < 10 do
  14                         variant { 10 - !i  }
  15                         i := !i + 1;
  16                         j := !j + 2;
  17                 done;
  18                 while 1 < !i do
  19                         variant { !i  }
  20                         i := !i - 1;
  21                         j := !j - 2;
  22                 done;
  23                 !j
  24
  25 end