bench/infer/mult.mlw

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