bench/infer/junjie.mlw

   1 module Junjie
   2         use ref.Ref
   3         use int.Int
   4
   5         let b [@bddinfer] [@infer](_:int):int
   6         ensures { result = 102 }
   7         =
   8                 let x = ref 0 in
   9                 let y = ref 0 in
  10                 while !y >= 0 do
  11                 variant { 0 }
  12                         if !x <= 50 then
  13                                 y := !y + 1
  14                         else
  15                                 y := !y - 1;
  16                         x := !x + 1;
  17                 done;
  18                 !y
  19 end