引理-计算序列中非负元素的个数

方法count(a)的作用是：输入一个整型序列a，返回a中非负元素的个数。

在Dafny中表示序列a长度的方法为|a|，再结合序列的切片和递归的思路，容易写出下面的count()方法：当a的长度为0时返回0，否则将a分割成第一个元素和剩下的元素，对单个元素可直接判断它的非负性，对多个元素则对它递归求解，最后返回它们的和。

function count(a :seq<int>): nat   // 返回序列a中非负元素个数
{
    if |a| == 0 then 0 else
    (if a[0] >= 0 then 1 else 0) + count(a[1..])
}

method m1(){
    assert count([0, -1, 1] + [-1, 2]) == 3;    // error!
}

对于上面的count()用类似assert count([1, -1, 0]) == 2这样的断言是可以验证通过的，但是如果用类似assert count([0, -1, 1] + [-1, 2]) == 3这样涉及序列拼接的断言是不能验证通过的，其原因在于序列拼接的+和count()中整型的+含义不同，count()并没有规定参数中序列的“相加”。

为了让Dafny能够验证上述断言，我们需要引进引理lemma，一种用于证明某种性质以供后续验证的方法。

在上述断言中，我们使用count()时默认了它对于+的分配性质，因此我们需要对于它的分配性先给出证明，以使Dafny能够正确识别有关断言，如下。

// 引理
lemma Distributive(a: seq<int>, b: seq<int>)    // 证明'+'对于count()是可分配的
    ensures count(a + b) == count(a) + count(b)
{
    if a == []
    {
        assert a + b == b;
    }   
    else
    {
        Distributive(a[1..], b);
        assert a + b == [a[0]] + (a[1..] + b);
    }
}

分配律性质需要确保count(a + b) == count(a) + count(b)，这是我们想要的结果。首先，若序列a为空，则验证断言a + b == b，否则切去a的首位元素，递归调用Distributive()，即验证后面所有序列的分配性，验证断言assert a + b == [a[0]] + (a[1..] + b)即序列拼接的正确性。整个递归的流程相当于是为Dafny提供了验证思路。

方法m1中，我们先调用Distributive()证明count()对于相关序列的分配律，再验证断言。

method m1(){
    Distributive([0, -1, 1], [-1, 2]);  // 先用引理证明分配律
    assert count([0, -1, 1] + [-1, 2]) == 3;    
}

验证通过。