examples/coincidence_count.mlw

   1
   2 (** Coincidence count
   3
   4     Exercise proposed by Rustan Leino at Dagstuhl seminar 14171, April 2014
   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     Authors: Jean-Christophe Filliâtre (CNRS)
  12              Andrei Paskevich (Université Paris Sud)
  13 *)
  14
  15 module CoincidenceCount
  16
  17   use int.Int
  18   use array.Array
  19   use ref.Refint
  20   use set.FsetInt
  21
  22   function setof (a: array 'a) : fset 'a =
  23     map (fun x -> a[x]) (interval 0 (length a))
  24
  25   function drop (a: array 'a) (n: int) : fset 'a =
  26     map (fun x -> a[x]) (interval n (length a))
  27
  28   lemma drop_left:
  29     forall a: array 'a, n: int. 0 <= n < length a ->
  30     drop a n == add a[n] (drop a (n+1))
  31
  32   predicate increasing (a: array int) =
  33     forall i j. 0 <= i < j < length a -> a[i] < a[j]
  34
  35   function cc (a b: array int) : int =
  36     cardinal (inter (setof a) (setof b))
  37
  38   lemma not_mem_inter_r:
  39     forall a: array int, i: int, s: fset int. 0 <= i < length a ->
  40     not (mem a[i] s) -> inter (drop a i) s == inter (drop a (i+1)) s
  41
  42   lemma not_mem_inter_l:
  43     forall a: array int, i: int, s: fset int. 0 <= i < length a ->
  44     not (mem a[i] s) -> inter s (drop a i) == inter s (drop a (i+1))
  45
  46   let coincidence_count (a b: array int) : int
  47     requires { increasing a }
  48     requires { increasing b }
  49     ensures  { result = cc a b }
  50   =
  51     let ref i = 0 in
  52     let ref j = 0 in
  53     let ref c = 0 in
  54     while i < length a && j < length b do
  55       invariant { 0 <= i <= length a }
  56       invariant { 0 <= j <= length b }
  57       invariant { c + cardinal (inter (drop a i) (drop b j)) = cc a b }
  58       variant   { length a - i + length b - j }
  59       if a[i] < b[j] then
  60         incr i
  61       else if a[i] > b[j] then
  62         incr j
  63       else begin
  64         assert { inter (drop a i) (drop b j) ==
  65                  add a[i] (inter (drop a (i+1)) (drop b (j+1))) };
  66         assert { not (mem a[i] (drop a (i+1))) };
  67         incr i;
  68         incr j;
  69         incr c
  70       end
  71     done;
  72     c
  73
  74 end
  75
  76 (** Variant using bags, from Rustan Leino's book "Program Proofs" *)
  77
  78 module CoincidenceCountBag
  79
  80   use int.Int
  81   use array.Array
  82   use ref.Refint
  83   use bag.Bag
  84
  85   predicate increasing (a: array int) =
  86     forall i j. 0 <= i < j < length a -> a[i] <= a[j]
  87
  88   let rec ghost function bagofsub (a: array 'a) (lo hi: int) : bag 'a
  89     requires { 0 <= lo <= hi <= length a } variant { hi - lo }
  90   = if lo >= hi then empty_bag else add a[lo] (bagofsub a (lo + 1) hi)
  91
  92   function bagof (a: array 'a) : bag 'a =
  93     bagofsub a 0 (length a)
  94
  95   function drop (a: array 'a) (i: int) : bag 'a =
  96     bagofsub a i (length a)
  97
  98   lemma not_mem_inter_r:
  99     forall a: array int, i: int, s: bag int. 0 <= i < length a ->
 100     not (mem a[i] s) -> inter (drop a i) s == inter (drop a (i+1)) s
 101
 102   lemma not_mem_inter_l:
 103     forall a: array int, i: int, s: bag int. 0 <= i < length a ->
 104     not (mem a[i] s) -> inter s (drop a i) == inter s (drop a (i+1))
 105
 106   let rec lemma bagofincreasing (a: array int) (i x: int)
 107     requires { increasing a }
 108     requires { 0 <= i < length a }
 109     requires { x < a[i] }
 110     ensures  { not (mem x (drop a i)) }
 111     variant  { length a - i }
 112   = if i < length a - 1 then bagofincreasing a (i+1) x
 113
 114   let coincidence_count (a b: array int) : int
 115     requires { increasing a }
 116     requires { increasing b }
 117     ensures  { result = card (inter (bagof a) (bagof b)) }
 118   =
 119     let ref i = 0 in
 120     let ref j = 0 in
 121     let ref c = 0 in
 122     while i < length a && j < length b do
 123       invariant { 0 <= i <= length a }
 124       invariant { 0 <= j <= length b }
 125       invariant { c + card (inter (drop a i) (drop b j))
 126                   = card (inter (bagof a) (bagof b)) }
 127       variant   { length a - i + length b - j }
 128       if a[i] < b[j] then
 129         incr i
 130       else if a[i] > b[j] then
 131         incr j
 132       else begin
 133         assert { inter (drop a i) (drop b j) ==
 134                  add a[i] (inter (drop a (i+1)) (drop b (j+1))) };
 135         incr i;
 136         incr j;
 137         incr c
 138       end
 139     done;
 140     c
 141
 142 end