How to verify a CountBy function/method?

[vkensou]

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 CountBy(items: array<int>, item: int) returns (r: nat)
    ensures r <= items.Length
    ensures r > 0  ==> exists k: nat :: k < items.Length && items[k] == 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
        decreases items.Length - i
        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;
}

method Main()
{
    var w := new int[3];
    w[0] := 1;
    w[1] := 2;
    w[2] := 1;

    var e := CountBy(w, 1);
    assert e == 2;
    assert count(w[..], 1) == 2;
}

there are errors:

Error: assertion might not hold
   |
37 |     assert e == 2;
   |            ^^^^^^
Error: assertion might not hold
   |
38 |     assert count(w[..], 1) == 2;
   |            ^^^^^^^^^^^^^^^^^^^^

In addition, I want use CountBy both in method statements and ensures/requires clauses. how could I down? Do I have to write it twice like the code above?

[vkensou]

I write a array version, but it's still not work.

function countArraySliceWithLast<T1, T2>(eq: (T1, T2) -> bool, item: T2, items: array<T1>, start: nat, end: nat, last: nat): (r: nat)
    requires start <= items.Length
    requires end <= items.Length
    requires start <= end
    requires start < items.Length ==> last < items.Length
    requires start == items.Length ==> last <= items.Length
    decreases items.Length - start
    reads items
    ensures r == 0 ==> forall k: nat :: k < items.Length ==> !eq(items[k], item)
    ensures 0 <= r <= items.Length
    ensures r > 0  ==> exists k: nat :: k < items.Length && eq(items[k], item)
    ensures r == countArraySliceWithLast(eq, item, items, start, end, last)
    ensures r == items.Length ==> forall k: nat :: k < items.Length ==> eq(items[k], item)
{
    if start == end then
        0
    else
        countArraySliceWithLast(eq, item, items, start + 1, end, (if eq(items[start], item) then 1 else 0) + last)
}