bench/infer/while5.mlw

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