bench/infer/while1.mlw

   1 module While1
   2
   3         use int.Int
   4         use ref.Ref
   5
   6         let b [@infer] [@bddinfer] (_:int) : int
   7         ensures { result = 18 }
   8         =
   9                 let i = ref 1 in
  10                 let j = ref 0 in
  11                 while !i < 10 do
  12                         variant { 10 - !i  }
  13                         i := !i + 1;
  14                         j := !j + 2;
  15                 done;
  16                 !j
  17
  18         let b2 [@infer:oct] [@bddinfer] (_:int) : int
  19         ensures { result = 18 }
  20         =
  21                 let i = ref 1 in
  22                 let j = ref 0 in
  23                 while !i < 10 do
  24                         variant { 10 - !i  }
  25                         i := !i + 1;
  26                         j := !j + 2;
  27                 done;
  28                 !j
  29
  30         let b3 [@infer:box] [@bddinfer] (_:int) : int
  31         ensures { result = 18 }
  32         =
  33                 let i = ref 1 in
  34                 let j = ref 0 in
  35                 while !i < 10 do
  36                         variant { 10 - !i  }
  37                         i := !i + 1;
  38                         j := !j + 2;
  39                 done;
  40                 !j
  41
  42 end