bench/infer/while7.mlw

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