Dafny and counting of occurrences

Question

I've been looking at the use of lemmas in Dafny but am finding it hard to understand and obviously the below example doesn't verify, quite possibly because Dafny doesn't see the induction or something like a lemma to prove some property of count? Basically, I don't know how or what I need to define to help convince Dafny that counting is inductive and a thing etc. Some of the ensures and invariants specifications are not necessary, but that's not the point. btw, this was easier in Spec#.

function count(items: seq<int>, item: int): nat
  decreases |items|
{
  if |items| == 0 then 0 else
    (if items[|items| - 1] == item then 1 else 0)
        + count( items[..(|items| - 1)], item )
}

method occurences(items: array<int>, item: int) returns (r: nat)
  requires items != null
  ensures r <= items.Length
  // some number of occurences of item
  ensures r > 0  ==> exists k: nat :: k < items.Length
                     && items[k] == item
  // no occurences of item
  ensures r == 0 ==> forall k: nat :: k < items.Length
                     ==> items[k] != item
  ensures r == count( items[..], item )
{
  var i: nat := 0;
  var num: nat := 0;

  while i < items.Length
    // i is increasing and there could be elements that match
    invariant num <= i <= items.Length
    invariant num > 0 ==> exists k: nat :: k < i
                          && items[k] == item
    invariant num == 0 ==> forall k: nat :: k < i
                           ==> items[k] != item
    invariant num == old(num) + 1 || num == old(num)
    invariant num == count( items[..i], item )
  {
    if items[i] == item
      { num := num + 1; }
    i := i + 1;
  }
  return num;
}

Answer 1

I would use a definition of count based around a multiset, then everything works:

function count(items: seq<int>, item: int): nat
  decreases |items|
{
  multiset(items)[item]
}

method occurences(items: array<int>, item: int) returns (r: nat)
  requires items != null
  ensures r <= items.Length
  // some number of occurences of item
  ensures r > 0  ==> exists k: nat :: k < items.Length
                     && items[k] == item
  // no occurences of item
  ensures r == 0 ==> forall k: nat :: k < items.Length
                     ==> items[k] != item
  ensures r == count(items[..], item)
{
  var i: nat := 0;
  var num: nat := 0;

  while i < items.Length
    // i is increasing and there could be elements that match
    invariant num <= i <= items.Length
    invariant num > 0 ==> exists k: nat :: k < i
                          && items[k] == item
    invariant num == 0 ==> forall k: nat :: k < i
                           ==> items[k] != item
    invariant num == old(num) + 1 || num == old(num)
    invariant num == count(items[..i], item)
  {
    if items[i] == item
      { num := num + 1; }
    i := i + 1;
  }
  assert items[..i] == items[..];
  r := num;
}

I would also like to suggest two alternative approaches, and another solution to your original design.

1. Without changing the implementation, I personally would probably write the specification like this:

   function count(items: seq<int>, item: int): nat
     decreases |items|
   {
     multiset(items)[item]
   }
   
   method occurences(items: array<int>, item: int) returns (num: nat)
     requires items != null
     ensures num <= items.Length
     ensures num == 0 <==> item !in items[..]
     ensures num == count(items[..], item)
   {
     num := 0;
   
     var i: nat := 0;
     while i < items.Length
       invariant num <= i <= items.Length
       invariant num == 0 <==> item !in items[..i]
       invariant num == count(items[..i], item)
     {
       if items[i] == item
         { num := num + 1; }
       i := i + 1;
     }
     assert items[..i] == items[..];
   }
   

2. If I were to decide on the implementation too then I would write it like this:

   method occurences(items: array<int>, item: int) returns (num: nat)
     requires items != null
     ensures num == multiset(items[..])[item]
   {
     num := multiset(items[..])[item];
   }
   

3. There is a way to get the original to verify by adding an extra assertion. NB. I think that "old" doesn't do what you think it does in a loop invariant.

   function count(items: seq<int>, item: int): nat
     decreases |items|
   {
     if |items| == 0 then 0 else
       (if items[|items|-1] == item then 1 else 0)
           + count(items[..|items|-1], item )
   }
   
   method occurences(items: array<int>, item: int) returns (r: nat)
     requires items != null
     ensures r <= items.Length
     // some number of occurences of item
     ensures r > 0  ==> exists k: nat :: k < items.Length
                        && items[k] == item
     // no occurences of item
     ensures r == 0 ==> forall k: nat :: k < items.Length
                        ==> items[k] != item
     ensures r == count( items[..], item )
   {
     var i: nat := 0;
     var num:nat := 0;
   
     while i < items.Length
       invariant num <= i <= items.Length
       invariant num > 0 ==> exists k: nat :: k < i
                             && items[k] == item
       invariant num == 0 ==> forall k: nat :: k < i
                              ==> items[k] != item
       invariant num == count(items[..i], item)
     {
       assert items[..i+1] == items[..i] + [items[i]];
   
       if items[i] == item
         { num := num + 1; }
       i := i + 1;
     }
     assert items[..i] == items[..];
     r := num;
   }