dafny 中的无效段计数

Question

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

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

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

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;
  }
}

dafny 中的无效段计数

invalid segment Count in dafny

formal-verification

count

dafny