coincidence_count_list.mlw 2.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10

(** Coincidence count

    Exercise proposed by Rustan Leino at Dagstuhl seminar 16131, March 2016

    You are given two sequences of integers, sorted in increasing
    order and without duplicate elements, and you count the number of
    elements that appear in both sequences (in linear time and constant
    space).

11
    See also coincidence_count.mlw for a version using arrays.
12 13 14 15 16 17

    Authors: Jean-Christophe Filliâtre (CNRS)
*)

module CoincidenceCount

18
  use list.List
19
  use set.SetAppInt
20
  use list.Elements
21
  use list.Mem as L
22
  use int.Int
23 24 25 26

  clone export list.Sorted
     with type t = int, predicate le = (<), goal Transitive.Trans

27
  let rec coincidence_count (a b: list int) : set
28 29 30
    requires { sorted a }
    requires { sorted b }
    ensures  { result == inter (elements a) (elements b) }
31
    variant  { a, b }
32 33 34 35 36 37 38 39 40 41
  =
    match a, b with
    | Cons ha ta, Cons hb tb ->
       if ha = hb then
         add ha (coincidence_count ta tb)
       else if ha < hb then
         coincidence_count ta b
       else
         coincidence_count a tb
    | _ ->
42
       empty ()
43 44 45
    end

end
46 47 48 49 50

(* the same, with elements of any type *)

module CoincidenceCountAnyType

51 52
  use list.List
  use list.Elements
53
  use list.Mem as L
54
  use int.Int
55

56 57 58 59
  type t

  val predicate eq (x y : t)
    ensures { result <-> x = y }
60 61 62

  clone set.SetApp with type elt = t, val eq = eq

63 64
  val predicate rel (x y : t)

65
  clone relations.TotalStrictOrder with type t, predicate rel, axiom .
66 67 68 69

  clone export list.Sorted
     with type t = t, predicate le = rel, goal Transitive.Trans

70
  let rec coincidence_count (a b: list t) : set
71 72 73 74 75 76 77
    requires { sorted a }
    requires { sorted b }
    ensures  { result == inter (elements a) (elements b) }
    variant  { a, b }
  =
    match a, b with
    | Cons ha ta, Cons hb tb ->
78
       if eq ha hb then
79 80 81 82 83 84
         add ha (coincidence_count ta tb)
       else if rel ha hb then
         coincidence_count ta b
       else
         coincidence_count a tb
    | _ ->
85
       empty ()
86 87 88 89 90 91 92 93
    end

end

(* the same, using only lists *)

module CoincidenceCountList

94 95 96
  use list.List
  use list.Mem
  use int.Int
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119

  clone export list.Sorted
     with type t = int, predicate le = (<), goal Transitive.Trans

  let rec coincidence_count (a b: list int) : list int
    requires { sorted a }
    requires { sorted b }
    ensures  { forall x. mem x result <-> mem x a /\ mem x b }
    variant  { a, b }
  =
    match a, b with
    | Cons ha ta, Cons hb tb ->
       if ha = hb then
         Cons ha (coincidence_count ta tb)
       else if ha < hb then
         coincidence_count ta b
       else
         coincidence_count a tb
    | _ ->
       Nil
    end

end