tests/sum_list00.mlw

   1 theory SumList
   2
   3 use export int.Int
   4 use export real.RealInfix
   5 use export list.List
   6 use export list.Length
   7 use export list.Nth
   8
   9 type or_integer_float = Integer int | Real real
  10
  11 (* nth element of the list *)
  12 function get_nth (i: int) (e: list or_integer_float) : or_integer_float =
  13 match nth i e with
  14 | None -> Integer (-1)
  15 | Some x -> x
  16 end
  17
  18 (* no integer zero till x (excluding) *)
  19 predicate no_zero_int (e: list or_integer_float) (x: int) =
  20 forall j: int. 0 <= j < x /\ x < length(e) ->
  21 match nth j e with
  22 | None -> true
  23 | Some y -> match y with
  24             | (Integer n) -> n <> 0
  25             | (Real r) -> true
  26             end
  27 end
  28
  29 (* no real less than 0.5 till x (excluding) *)
  30 predicate no_zero_real (e: list or_integer_float) (x: int) =
  31 forall j: int. 0 <= j < x /\ x < length(e) ->
  32 match nth j e with
  33 | None -> true
  34 | Some y -> match y with
  35             | (Integer n) -> true
  36             | (Real r) -> r >=. 0.5
  37             end
  38 end
  39
  40 (* no integer zero and no real less than 0.5 till x (excluding) *)
  41 predicate no_zero (e: list or_integer_float) (x: int) =
  42 forall j: int. 0 <= j < x /\ x < length(e) ->
  43 match nth j e with
  44 | None -> true
  45 | Some y -> match y with
  46             | (Integer n) -> n <> 0
  47             | (Real r) -> r >=. 0.5
  48             end
  49 end
  50
  51 (* integer zero at  x *)
  52 predicate zero_at_int (e: list or_integer_float) (x: int) =
  53 match nth x e with
  54 | None -> false
  55 | Some y -> match y with
  56             | (Integer n) -> n = 0
  57             | (Real r) -> false
  58             end
  59 end
  60
  61 (* real less than 0.5 at  x *)
  62 predicate zero_at_real (e: list or_integer_float) (x: int) =
  63 match nth x e with
  64 | None -> false
  65 | Some y -> match y with
  66             | (Integer n) -> false
  67             | (Real r) -> r <. 0.5
  68             end
  69 end
  70
  71
  72 (* sum integers in a list *)
  73 function add_int (e: list or_integer_float) (i: int) (j: int) : int =
  74 if i < j then
  75   match e with
  76   | Nil -> 0
  77   | Cons (Integer n) t -> if n = 0 then 0 else n + add_int t (i+1) j
  78   | Cons _ t -> add_int t (i+1) j
  79   end
  80 else
  81 0
  82
  83 (* sum reals in a list *)
  84 function add_real (e: list or_integer_float) (i: int) (j: int) : real =
  85 if i < j then
  86   match e with
  87   | Nil -> 0.0
  88   | Cons (Real x) t -> if x <. 0.5 then 0.0 else x +. add_real t (i+1) j
  89   | Cons _ t -> add_real t (i+1) j
  90   end
  91 else
  92 0.0
  93
  94 end
  95
  96 module SumList
  97
  98 use SumList
  99 use module ref.Ref
 100
 101 val status: ref int
 102
 103 exception Break
 104
 105 let sum (l: list or_integer_float) : (int, real) =
 106   { true }
 107   status := 0;
 108   let si = ref 0 in
 109   let sf = ref 0.0 in
 110   let x = ref (any or_integer_float) in
 111   try
 112     for i = 0 to length(l) - 1 do
 113     invariant { !si = add_int (l) (0) (!status) /\ !sf = add_real (l) (0) (!status)
 114                 /\ 0 <= !status < length(l)
 115               }
 116      status := i;
 117      x := get_nth i l;
 118      match !x with
 119         | (Integer n) -> if n = 0 then raise Break else si := !si + n
 120         | (Real r) -> if r <. 0.5 then raise Break else sf := !sf +. r
 121      end
 122    done;
 123    status := -1;
 124    (!si, !sf)
 125   with Break -> (!si, !sf)
 126   end
 127   { let (si, sf) = result in
 128         ( !status = -1 /\ si = add_int (l) (0) (length(l)) /\ sf = add_real (l) (0) (length(l))
 129                 /\ no_zero (l) (length(l)) ) \/
 130         ( 0 <= !status < length(l) /\ si = add_int (l) (0) (!status) /\ sf = add_real (l) (0) (!status)
 131                 /\ no_zero_int (l) (!status) /\ no_zero_real (l) (!status)
 132                 /\ ( zero_at_int (l) (!status) \/ zero_at_real (l) (!status) ) )
 133   }
 134
 135
 136 let main () =
 137   let l =
 138     Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
 139       (Cons (Real 1.4) (Cons (Integer 9) Nil))))
 140   in
 141   let (s,f) = sum l in
 142   assert { s = 22 };
 143   assert { f = 4.7 }
 144
 145 end