bench/infer/tuple2.mlw

   1 module Tuple2
   2
   3         use int.Int
   4         use ref.Ref
   5
   6         val c(_:int) : (int, int)
   7         ensures { result = (1, 2) }
   8
   9         let b [@bddinfer] [@infer](_:int) : int
  10         ensures { result = 20 }
  11         =
  12         let _ = () in
  13         let _= c 4 in
  14                 let i = ref 0 in
  15                 let j = ref 0 in
  16                 i := 0;
  17                 j := 0;
  18                 while !i < 10 do
  19                         variant { 10 - !i }
  20                         let (a, b) = (!i + 1, !j + 2) in
  21                         i := a;
  22                         j := b;
  23                 done;
  24                 !j
  25
  26         let b2 [@bddinfer] [@infer:oct](_:int) : int
  27         ensures { result = 20 }
  28         =
  29         let _ = () in
  30         let _= c 4 in
  31                 let i = ref 0 in
  32                 let j = ref 0 in
  33                 i := 0;
  34                 j := 0;
  35                 while !i < 10 do
  36                         variant { 10 - !i }
  37                         let (a, b) = (!i + 1, !j + 2) in
  38                         i := a;
  39                         j := b;
  40                 done;
  41                 !j
  42
  43         let b3 [@bddinfer] [@infer:box](_:int) : int
  44         ensures { result = 20 }
  45         =
  46         let _ = () in
  47         let _= c 4 in
  48                 let i = ref 0 in
  49                 let j = ref 0 in
  50                 i := 0;
  51                 j := 0;
  52                 while !i < 10 do
  53                         variant { 10 - !i }
  54                         let (a, b) = (!i + 1, !j + 2) in
  55                         i := a;
  56                         j := b;
  57                 done;
  58                 !j
  59
  60 end