invalid segment Count in dafny

Question

i wrote the following proof for the code in the link below. i would like to get some help with prooving the count2 method . the alternation proof is not so clear to me thanks

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

When you are looping backwards you have to decrement the index before using it to access the array

i, c := i0-1, c0

Because you are looping backwards you have to decrement the counter before you access the array. You can see this by examining the method precondition. Given

0 < i0 <= a.Length

the array access a[i0] is not gaurenteed to be in range, since i0==a.Length is possible. Furthermore you need a[0] to be included in the product, but i0 is never 0.

However, given the same precondition the array access a[i0-1] makes sense since

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

You also need to increment rather than decrement the occurrence count

c := c + 1;

Here is a version that verifies

http://rise4fun.com/Dafny/GM0vt

I think you may find it easier to verify these programs if you use a clearer programming style with less indirection (although perhaps you are doing an exercise on method pre and post conditions). My experience has been that part of successfully verifying an algorithm is first finding a nice, clear, way to express the algorithm.

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