线性查询

输入一个整型数组和一个整数key，返回该数组中等于key的元素所在的位置，显然数组的下标从0开始。

算法上，直接遍历该数组，判断当前元素是否等于key即可，若等于则程序返回，所得的n就是要求的位置，若不等于则往后寻找。

method LinearSearch(a: array<int>, key: int) returns (n: nat)   
ensures 0 <= n <= a.Length
ensures n == a.Length || a[n] == key
{
    n := 0;
    while n < a.Length
    invariant n <= a.Length
    decreases a.Length - n      //需保证该表达式递减且不小于0
    {
        if a[n] == key 
        {
            return;
        }
        n := n + 1;
    }
}

容易想到，n的数值是大于等于0的整数，且不能超过数组的长度，否则产生越界问题，所以要有ensures 0 <= n <= a.Length。

其次，程序返回的条件要么是找到了对应的位置，查找成功；要么是n的值达到了数组的长度还没有找到相应元素，查找失败。因此要有ensures n == a.Length || a[n] == key

函数主体部分，我们在遍历时使用的是while语句，这里涉及到循环不变体invariant的使用，Dafny在执行循环时每次都会判断循环不变体是否满足条件，以判断循环内是否有错误，因此我们加上invariant n <= a.Length是更严谨的做法。同时，由于每次循环后n增大，需要加上decreases a.Length - n保证数组长度 - n是减小的，同时不会比0小。