examples/add_list_vc_sp.mlw

   1 theory SumList
   2
   3 use export int.Int
   4 use export real.RealInfix
   5 use export list.List
   6
   7 type or_integer_float = Integer int | Real real
   8
   9
  10 (* sum integers in a list *)
  11 function add_int (e: list or_integer_float) : int =
  12   match e with
  13   | Nil -> 0
  14   | Cons (Integer n) t -> n + add_int t
  15   | Cons _ t -> add_int t
  16   end
  17
  18 (* sum reals in a list *)
  19 function add_real (e: list or_integer_float) : real =
  20   match e with
  21   | Nil -> 0.0
  22   | Cons (Real x) t -> x +. add_real t
  23   | Cons _ t -> add_real t
  24   end
  25
  26 end
  27
  28 module AddListRec
  29
  30 use SumList
  31
  32 let rec sum (l: list or_integer_float) : (si: int, sf: real) =
  33     variant { l }
  34     ensures { si = add_int l /\ sf = add_real l }
  35   [@vc:sp]
  36   match l with
  37   | Nil -> 0, 0.0
  38   | Cons h t ->
  39       let a,b = sum t in
  40       match h with
  41       | Integer n -> n + a, b
  42       | Real x -> a, x +. b
  43       end
  44   end
  45
  46 let main () =
  47   [@vc:sp]
  48   let l =
  49     Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
  50       (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  51   in
  52   let s,f = sum l in
  53   assert { s = 22 };
  54   assert { f = 4.7 }
  55
  56 end
  57
  58
  59 module AddListImp
  60
  61 use SumList
  62 use ref.Ref
  63
  64 let sum (l: list or_integer_float) : (si: int, sf: real) =
  65     ensures { si = add_int l /\ sf = add_real l }
  66   [@vc:sp]
  67   let si = ref 0 in
  68   let sf = ref 0.0 in
  69   let ll = ref l in
  70   while True do
  71     invariant { !si + add_int !ll = add_int l /\
  72                 !sf +. add_real !ll = add_real l }
  73     variant { !ll }
  74      match !ll with
  75      | Nil -> return !si, !sf
  76      | Cons (Integer n) t ->
  77          si := !si + n; ll := t
  78      | Cons (Real x) t ->
  79          sf := !sf +. x; ll := t
  80      end
  81   done;
  82   absurd
  83
  84
  85 let main () =
  86   [@vc:sp]
  87   let l =
  88     Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
  89       (Cons (Real 1.4) (Cons (Integer 9) Nil))))
  90   in
  91   let s,f = sum l in
  92   assert { s = 22 };
  93   assert { f = 4.7 }
  94
  95 end