histogram.dfy

// *** Arrays that are all zeroes

predicate all_zeroes_up_to(a: array<nat>, stop: nat)
  reads a
  requires 0 <= stop <= a.Length
{
  forall i :: 0 <= i < stop ==> a[i] == 0
}

predicate all_zeroes(a: array<nat>)
  reads a
{
  all_zeroes_up_to(a, a.Length)
}

method Zeroes(len: nat) returns (a: array<nat>)
  ensures a.Length == len && all_zeroes(a)
{
  a := new nat[len];
  var i := 0;
  while i < a.Length
    invariant 0 <= i <= a.Length
    invariant all_zeroes_up_to(a, i)
  {
    a[i] := 0;
    i := i + 1;
  }
}


// *** Histograms

function count_value_in_prefix(a: array<nat>, v: nat, len: nat): nat
  requires 0 <= len <= a.Length
  reads a
  decreases len
{
  if len == 0 then 0
  else if a[len - 1] == v then count_value_in_prefix(a, v, len - 1) + 1
  else count_value_in_prefix(a, v, len - 1)
}

function count_value(a: array<nat>, v: nat): nat
  reads a
{
  count_value_in_prefix(a, v, a.Length)
}

predicate greater_than_all(limit: nat, a: array<nat>)
  reads a
{
  forall i :: 0 <= i < a.Length ==> a[i] < limit
}

predicate histogram_of_prefix(h: array<nat>, a: array<nat>, len: nat)
  requires 0 <= len <= a.Length
  reads h, a
{
  greater_than_all(h.Length, a)
  && forall n :: 0 <= n < h.Length ==> h[n] == count_value_in_prefix(a, n, len)
}

predicate histogram_of(h: array<nat>, a: array<nat>)
  reads h, a
{
  greater_than_all(h.Length, a)
  && forall n :: 0 <= n < h.Length ==> h[n] == count_value(a, n)
}

method Histogram(a: array<nat>, limit: nat) returns (h: array<nat>)
  requires greater_than_all(limit, a)
  ensures h.Length == limit && histogram_of(h, a)
{
  h := Zeroes(limit);
  assert histogram_of_prefix(h, a, 0);

  var i := 0;
  while i < a.Length
    invariant 0 <= i <= a.Length
    invariant histogram_of_prefix(h, a, i)
  {
    var n := a[i];
    h[n] := h[n] + 1;
    i := i + 1;
  }
}