tests/example-add.mlw

   1 module TestModule
   2
   3 (* module imports *)
   4 use int.Int
   5
   6 use module ref.Ref
   7
   8 use bool.Bool
   9
  10 use list.List
  11 use list.Length
  12 use list.Nth
  13
  14 use real.RealInfix
  15 use real.Abs
  16
  17 (* global variables declarations *)
  18 val status : ref int
  19
  20 (* variables type declarations *)
  21 type mm_integer = int
  22 type mm_float = real
  23
  24 type or_integer_float = Integer mm_integer | Real mm_float
  25 type list_or_integer_float = list or_integer_float
  26
  27 (* exceptions type declarations *)
  28 type return_type = (int, real)
  29
  30 (* exceptions declarations *)
  31 exception BreakLoop return_type
  32
  33
  34 (* logical definitions of type tests  *)
  35 function type_test_or_integer_float_to_integer (x: or_integer_float) : bool =
  36         match x with
  37         | Integer mm_integer -> True
  38         | Real mm_float -> False
  39         end
  40
  41 function type_test_or_integer_float_to_float (x: or_integer_float) : bool =
  42         match x with
  43         | Integer mm_integer -> False
  44         | Real mm_float -> True
  45         end
  46
  47 (* auxiliary definitions and declarations *)
  48 function get_nth (i: int) (l: list_or_integer_float) : or_integer_float =
  49 match nth i l with
  50 | None -> Real 0.0
  51 | Some x -> x
  52 end
  53
  54 axiom def_nth0: forall i: int, l: list_or_integer_float. 0 <= i < length(l) -> nth i l <> None
  55
  56 (*axiom def_length0: forall l: list_or_integer_float. length(l) > 0*)
  57
  58 (* logical type conversion functions *)
  59 function or_integer_float_to_integer (e: or_integer_float) : mm_integer =
  60 match e with
  61 | Integer mm_integer -> mm_integer
  62 | Real mm_float -> 1
  63 end
  64
  65 function or_integer_float_to_float (e: or_integer_float) : mm_float =
  66 match e with
  67 | Integer mm_integer -> 1.0
  68 | Real mm_float -> mm_float
  69 end
  70
  71 (* logical auxiliary functions for specification *)
  72 function add0 (e: list_or_integer_float) (i: int) (j: int) : mm_integer =
  73 if i < j then
  74 match e with
  75 | Nil -> 0
  76 | Cons h t -> if type_test_or_integer_float_to_integer (h) = True then
  77                 or_integer_float_to_integer (h) + add0 (t) (i+1) (j)
  78               else
  79                 add0 (t) (i+1) (j)
  80 end
  81 else
  82 0
  83
  84 function add1 (e: list_or_integer_float) (i: int) (j: int) : mm_float =
  85 if i < j then
  86 match e with
  87 | Nil -> 0.0
  88 | Cons h t -> if type_test_or_integer_float_to_float (h) = True then
  89                 or_integer_float_to_float (h) +. add1 (t)(i+1)(j)
  90               else
  91                 add1 (t)(i+1)(j)
  92 end
  93 else
  94 0.0
  95
  96 (* logical translation of procedure "sum (l: list(Or(integer, float)):[integer, float]" *)
  97 let sum (l: list_or_integer_float) : (int, real) =
  98 {true}
  99         try
 100           status := 0;
 101             let si = ref 0 in
 102               let sf = ref 0.0 in
 103                 let x = ref (any or_integer_float) in
 104                 for i = 0 to length(l)-1 do
 105                 invariant { !status >= 0 && (!si = add0(l)(0)(i) && !sf = add1(l)(0)(i) &&
 106         (forall i0: int . 0 <= i0 < i -> ( type_test_or_integer_float_to_integer (get_nth i0 l) = True ->
 107                                         or_integer_float_to_integer (get_nth i0 l) <> 0 ) )
 108         && (forall i0: int . 0 <= i0 < i -> ( type_test_or_integer_float_to_float (get_nth i0 l) = True ->
 109                                         or_integer_float_to_float (get_nth i0 l) >=. 0.5 ) ) )}
 110                   status := i;
 111                   x := get_nth i l;
 112                         if type_test_or_integer_float_to_integer (!x) = True then
 113                           if or_integer_float_to_integer (!x) = 0 then
 114                             raise (BreakLoop (!si,!sf))
 115                           else
 116                             si := !si + or_integer_float_to_integer (!x)
 117                         else
 118                           if type_test_or_integer_float_to_float (!x) = True then
 119                             if or_integer_float_to_float (!x) <. 0.5 then
 120                               raise (BreakLoop (!si,!sf))
 121                             else
 122                               sf := !sf +. or_integer_float_to_float (!x)
 123                 done;
 124                 status := -1;
 125                 (!si,!sf)
 126         with BreakLoop excp ->
 127         match excp with
 128         | (a0, a1) -> (a0, a1)
 129         end
 130         end
 131 {
 132 let (si0, sf0) = result in
 133 ( !status = -1
 134   && si0 = add0(l)(0)(length(l))
 135   && sf0 = add1(l)(0)(length(l))
 136   && (forall i0: int . 0 <= i0 < length(l) ->  ( type_test_or_integer_float_to_integer (get_nth i0 l) = True ->
 137    or_integer_float_to_integer (get_nth i0 l) <> 0 ) )
 138   && (forall i0: int . 0 <= i0 < length(l) -> ( type_test_or_integer_float_to_float (get_nth i0 l) = True ->
 139    or_integer_float_to_float (get_nth i0 l) >=. 0.5 ) )
 140 )
 141 ||
 142 ( 0 <= !status < length(l)
 143   && si0 = add0(l)(0)(!status)
 144   && sf0 = add1(l)(0)(!status)
 145   && ( (type_test_or_integer_float_to_integer (get_nth !status l) = True
 146         && or_integer_float_to_integer (get_nth !status l) = 0)
 147       ||
 148        (type_test_or_integer_float_to_float (get_nth !status l) = True
 149         && or_integer_float_to_float (get_nth !status l) <. 0.5)
 150      )
 151   && (forall i0: int . 0 <= i0 < !status -> ( type_test_or_integer_float_to_integer (get_nth i0 l) = True ->
 152    or_integer_float_to_integer (get_nth i0 l) <> 0 ) )
 153   && (forall i0: int . 0 <= i0 < !status -> ( type_test_or_integer_float_to_float (get_nth i0 l) = True ->
 154    or_integer_float_to_float (get_nth i0 l) >=. 0.5 ) )
 155 )
 156 }
 157
 158 let main () =
 159   let l = Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8) (Cons (Real 1.4) (Cons (Integer 9) Nil)))) in
 160   let (s,f) = sum (l) in
 161   assert { !status = -1 };
 162   assert { s = 22 };
 163   assert { f = 4.7 }
 164
 165 end