examples/coincidence_count_list.mlw

   1
   2 (** Coincidence count
   3
   4     Exercise proposed by Rustan Leino at Dagstuhl seminar 16131, March 2016
   5
   6     You are given two sequences of integers, sorted in increasing
   7     order and without duplicate elements, and you count the number of
   8     elements that appear in both sequences (in linear time and constant
   9     space).
  10
  11     See also coincidence_count.mlw for a version using arrays.
  12
  13     Authors: Jean-Christophe Filliâtre (CNRS)
  14 *)
  15
  16 module CoincidenceCount
  17
  18   use list.List
  19   use set.SetAppInt
  20   use list.Elements
  21   use list.Mem as L
  22   use int.Int
  23
  24   clone export list.Sorted
  25      with type t = int, predicate le = (<), goal Transitive.Trans
  26
  27   let rec coincidence_count (a b: list int) : set
  28     requires { sorted a }
  29     requires { sorted b }
  30     ensures  { result == inter (elements a) (elements b) }
  31     variant  { a, b }
  32   =
  33     match a, b with
  34     | Cons ha ta, Cons hb tb ->
  35        if ha = hb then
  36          add ha (coincidence_count ta tb)
  37        else if ha < hb then
  38          coincidence_count ta b
  39        else
  40          coincidence_count a tb
  41     | _ ->
  42        empty ()
  43     end
  44
  45 end
  46
  47 (* the same, with elements of any type *)
  48
  49 module CoincidenceCountAnyType
  50
  51   use list.List
  52   use list.Elements
  53   use list.Mem as L
  54   use int.Int
  55
  56   type t
  57
  58   val predicate eq (x y : t)
  59     ensures { result <-> x = y }
  60
  61   clone set.SetApp with type elt = t, val eq = eq
  62
  63   val predicate rel (x y : t)
  64
  65   clone relations.TotalStrictOrder with type t, predicate rel, axiom .
  66
  67   clone export list.Sorted
  68      with type t = t, predicate le = rel, goal Transitive.Trans
  69
  70   let rec coincidence_count (a b: list t) : set
  71     requires { sorted a }
  72     requires { sorted b }
  73     ensures  { result == inter (elements a) (elements b) }
  74     variant  { a, b }
  75   =
  76     match a, b with
  77     | Cons ha ta, Cons hb tb ->
  78        if eq ha hb then
  79          add ha (coincidence_count ta tb)
  80        else if rel ha hb then
  81          coincidence_count ta b
  82        else
  83          coincidence_count a tb
  84     | _ ->
  85        empty ()
  86     end
  87
  88 end
  89
  90 (* the same, using only lists *)
  91
  92 module CoincidenceCountList
  93
  94   use list.List
  95   use list.Mem
  96   use int.Int
  97
  98   clone export list.Sorted
  99      with type t = int, predicate le = (<), goal Transitive.Trans
 100
 101   let rec coincidence_count (a b: list int) : list int
 102     requires { sorted a }
 103     requires { sorted b }
 104     ensures  { forall x. mem x result <-> mem x a /\ mem x b }
 105     variant  { a, b }
 106   =
 107     match a, b with
 108     | Cons ha ta, Cons hb tb ->
 109        if ha = hb then
 110          Cons ha (coincidence_count ta tb)
 111        else if ha < hb then
 112          coincidence_count ta b
 113        else
 114          coincidence_count a tb
 115     | _ ->
 116        Nil
 117     end
 118
 119 end