coincidence_count_list.mlw 2.65 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
18
19
20
21
22
23
24
25
26
27
28
29
30

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

module CoincidenceCount

  use import list.List
  use import set.Fset
  use import list.Elements
  use list.Mem as L
  use import int.Int

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

  let rec coincidence_count (a b: list int) : set int
    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
42
43
44
45
  =
    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
    | _ ->
       empty
    end

end
46
47
48
49
50
51
52
53
54
55
56

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

module CoincidenceCountAnyType

  use import list.List
  use import set.Fset
  use import list.Elements
  use list.Mem as L
  use import int.Int

57
58
59
60
61
62
  type t

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

63
  clone import relations.TotalStrictOrder with type t, predicate rel, axiom .
64
65
66
67
68
69
70
71
72
73
74
75

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

  let rec coincidence_count (a b: list t) : set t
    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 ->
76
       if eq ha hb then
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
         add ha (coincidence_count ta tb)
       else if rel ha hb then
         coincidence_count ta b
       else
         coincidence_count a tb
    | _ ->
       empty
    end

end

(* the same, using only lists *)

module CoincidenceCountList

  use import list.List
  use import list.Mem
  use import int.Int

  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