dafny 中的无效段计数

Question

我为下面链接中的代码编写了以下证明。 我想在证明 count2 方法方面获得一些帮助。交替证明对我来说不是很清楚 谢谢

http://rise4fun.com/Dafny/ueBY

method Main() {
    var a: array<int> := new int[4];
    a[0] := 7;
    a[1] := -2;
    a[2] := 3;
    a[3] := -2;
    assert a[..] == [7,-2,3,-2];

    var c := SumProdAndCount(a, -2);
    assert a[0] == 7 && a[1] == -2 && a[2] == 3 && a[3] == -2;
    assert c == RecursiveCount(-2, a, 0); // == 2
    print "\nThe number of occurrences of -2 in [7,-2,3,-2] is ";
    print c;
}

function RecursiveCount(key: int, a: array<int>, from: nat) : int
    reads a
    requires a != null
    requires from <= a.Length
    decreases a.Length-from
{
    if from == a.Length then 0
    else if a[from] == key then 1+RecursiveCount(key, a, from+1)
    else RecursiveCount(key, a, from+1)
}

method SumProdAndCount(a: array<int>, key: int) returns (c: nat)
    requires a != null
    ensures c == RecursiveCount(key, a, 0)
{
    // Introduce local variable (6.1)
    var i : nat;
    i, c := Count1(key, a);
    // Strengthen post condition (1.1)
    assert  i == 0 && c == RecursiveCount(key,a,i);
}


method Count1(key : int,a: array<int>)returns(i : nat, c : nat)
    requires a != null;
    ensures i == 0 && c == RecursiveCount(key,a,i) ;
{
//  leading assignment (8.5)
     c,i:= 0,a.Length;

//  Iteration (5.5)
    while (i >0)
    invariant 0 <= i <= a.Length && c == RecursiveCount(key,a,i);
    decreases i;
    {
     i, c := Count2(key,a, i, c);
    }
  assert i == 0 && c == RecursiveCount(key,a,i) ;
}

method Count2(key : int, a: array<int>, i0 : nat, c0 : nat) returns (i : nat, c : nat)
    requires a != null;
    requires 0 <i0 <= a.Length && c0==RecursiveCount(key,a,i0);
    ensures i=i0-1 && c==RecursiveCount(key,a,i);
{
     // Assignment (1.3)
    i, c := i0, c0;
    // Alternation (4.1)
    if (a[i] == key) {
        c := c - 1;
    }
    else {
        assert a[i] != key && 0 <i0 <= a.Length && c0==RecursiveCount(key,a,i0);
        //  skip command 3.2
    }
    // folowing assignment 8.5
    i := i0- 1;
}

Answer 1

当您向后循环时，您必须在 使用它访问数组之前减少索引

i, c := i0-1, c0

因为您正在向后循环，所以您必须在访问数组之前递减计数器。您可以通过检查方法前置条件来看到这一点。给定

0 < i0 <= a.Length

数组访问a[i0] 不在范围内，因为i0==a.Length 是可能的。此外，您需要将a[0] 包含在产品中，但i0 绝不是0。

但是，在相同的前提条件下，数组访问 a[i0-1] 是有意义的，因为

0 < i0 <= a.Length ==> 0 <= (i0-1) < a.Length

您还需要增加而不是减少出现次数

c := c + 1;

这是一个可以验证的版本

http://rise4fun.com/Dafny/GM0vt

我认为，如果您使用更清晰的编程风格和更少的间接性，我认为您可能会发现验证这些程序会更容易（尽管您可能正在对方法的前置条件和后置条件进行练习）。我的经验是，要成功验证算法，首先要找到一种清晰、清晰的算法表达方式。

http://rise4fun.com/Dafny/QCgc

method Main() {
    var a: array<int> := new int[4];
    a[0] := 7;
    a[1] := -2;
    a[2] := 3;
    a[3] := -2;
    assert a[..] == [7,-2,3,-2];

    var c := SumProdAndCount(a, -2);
    assert a[0] == 7 && a[1] == -2 && a[2] == 3 && a[3] == -2;
    assert c == RecursiveCount(-2, a, 0); // == 2
    print "\nThe number of occurrences of -2 in [7,-2,3,-2] is ";
    print c;
}

function RecursiveCount(key: int, a: array<int>, from: nat) : int
    reads a
    requires a != null
    requires from <= a.Length
    decreases a.Length-from
{
    if from == a.Length then 0
    else if a[from] == key then 1+RecursiveCount(key, a, from+1)
    else RecursiveCount(key, a, from+1)
}

method SumProdAndCount(a: array<int>, key: int) returns (c: nat)
    requires a != null
    ensures c == RecursiveCount(key, a, 0)
{
  c := 0;
  var i : nat := 0;
  ghost var r := RecursiveCount(key, a, 0);
  while (i < a.Length)
    invariant 0 <= i <= a.Length
    invariant r == c + RecursiveCount(key,a,i);
  {
       i, c := i+1, if a[i]==key then c+1 else c;
  }
}