0

以下のリンクのコードの次の証明を書きました。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;
}
4

1 に答える 1

0

逆方向にループしている場合は、インデックスを使用して配列にアクセスする前に、インデックスをデクリメントする必要があります

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;
  }
}
于 2015-12-15T16:13:12.027 に答える