multiply an array

Dec 12, 2015 at 6:16 PM
Edited Dec 20, 2015 at 9:25 AM
i wrote the following code , but dafny can't verify it , can you figure out what is wrong with my prove?
method product(a: array<int>, key: int) returns (p: int)
    requires a != null
    ensures p == RecursivePositiveProduct(a, 0)
{

// Introduce local variable (6.1)
    var i : nat;

// Sequential composition (3.3): mid: 0 <= i <= a.Length && p == RecursivePositiveProduct(a,i)

    assert  RecursivePositiveProduct(a,a.Length)==1 ;
    // leading assignment (8.5)
    p, i := 1,a.Length;
    assert  i <= a.Length ;
  assert  p == RecursivePositiveProduct(a,i)  ;  /*HERE I HAVE A PROBLEM */

// iteration (5.5)
    while (i != 0)
        invariant i <= a.Length  && p == RecursivePositiveProduct(a,i);
        decreases i;
    {
        p, i := Product1(p, a, i);
    }

// Strengthen post condition (1.1)
    assert  i <=a.Length &&  p == RecursivePositiveProduct(a,i) && i == 0 ;
}



method Product1(p0 : nat, a: array<int>, i0 : nat) returns (p : nat, i : nat)
  requires a!=null;
    requires i0 <= a.Length &&  p0 == RecursivePositiveProduct(a,i0) && i0!= 0;
    ensures i <=a.Length  &&  p == RecursivePositiveProduct(a,i) && 0<= i< i0;
{
    p, i := p0, i0;
    // Following assignment (3.5) + Contract frame (5.4)
    assert i <=a.Length && p0 == RecursivePositiveProduct(a,i) && i != 0;
    assert a[i..] == a[i-1..] + [a[i-1]];
    assert a[i] <= 0 ==> p0 == RecursivePositiveProduct(a,i-1) && a[i] > 0 ==> a[i]*p0 == RecursivePositiveProduct(a,i-1) ;
    
    // Alternation (4.1)
    if {
        case(a[i] > 0) =>
            p := p0 * a[i];
        case (a[i] <= 0) => 
            // Skip command (3.2)               
    }
assert a[i..] == a[i-1..] + [a[i-1]]  &&  0 <= i-1 <=a.Length && 
p == RecursivePositiveProduct(a,i)  &&  0 <= (i-1) < i;
    //followiong assignment (3.5)
    i := i - 1;
    assert 0 <= i <=a.Length && p == RecursivePositiveProduct(a,i) && 0 <=  i < i0;
}




THANKS!
Dec 13, 2015 at 8:37 PM
I think your while loop in product also needs this invariant invariant p >= 0;

However, I can't see how this assertion assert a[i..] == a[i-1..] + [a[i-1]] could ever be true. Perhaps I am confused, but I think that the slice a[i..] is one element smaller than the slice a[i-1..] so the sequence a[i-1..] + [a[i-1]] is two elements larger than the sequence a[i..]. What is your intention here?

http://rise4fun.com/Dafny/u8R
Dec 14, 2015 at 11:59 AM
Edited Dec 14, 2015 at 12:09 PM
well you are absolutely right! i tried to say something about the division ofthe array but maybe it is unnecessary ,
after thinking again i got this :

method product(a: array<int>, key: int) returns (p: int)
    requires a != null
    ensures p == RecursivePositiveProduct(a, 0)
{

// Introduce local variable (6.1)
    var i : nat;
    assert  RecursivePositiveProduct(a,a.Length)==1 ;
    p, i := 1,a.Length;
    assert  p == RecursivePositiveProduct(a,i) ; 

// iteration (5.5)
    while (i > 0)
        invariant i <= a.Length && p == RecursivePositiveProduct(a,i)
        invariant p>=0;
        decreases i;
    {
        p, i := Product1(p, a, i);
    }
// Strengthen post condition (1.1)
    assert  i ==0 && p == RecursivePositiveProduct(a,i) ;
}


method Product1(p0 : nat, a: array<int>, i0 : nat) returns (p : nat, i : nat)
  requires a!=null;
    requires  0 <i0 <=a.Length && p0 == RecursivePositiveProduct(a,i0) ;
    ensures i ==i0-1 && p == RecursivePositiveProduct(a,i) ;
{
    p, i := p0, i0;

  assert a[i] <= 0 ==> p0 == RecursivePositiveProduct(a,i) ;
  assert a[i] > 0 ==> a[i]*p0 == RecursivePositiveProduct(a,i) ;


    if {
        case(a[i] > 0) =>
            p := p0 * a[i];
        case (a[i] <= 0) => 
            // Skip command (3.2)               
    }
       i := i0 - 1;
}

still complicating with the product 1 proove :/

http://rise4fun.com/Dafny/JmTK
Dec 15, 2015 at 12:05 PM
I think that it should be p, i := p0, i0-1;

Here is a verifying version, using a ghost variable and forward iteration which you may prefer http://rise4fun.com/Dafny/iyHO
method product(a: array<int>, key: int) returns (p: int)
    requires a != null
    ensures p == RecursivePositiveProduct(a, 0)
{
    var i : nat;
    p, i := 1, 0;

    ghost var r := RecursivePositiveProduct(a,0);  
    while (i < a.Length)
        invariant i <= a.Length
        invariant p * RecursivePositiveProduct(a,i) == r
    {
        p, i := (if a[i] > 0 then a[i]*p else p), i+1;
    }
}

function RecursivePositiveProduct(a: array<int>, from: nat) : int
    reads a
    requires a != null
    requires from <= a.Length
    decreases a.Length-from
{
    if from == a.Length then 1
    else if a[from] <= 0 then RecursivePositiveProduct(a, from + 1)
    else a[from] * RecursivePositiveProduct(a, from + 1)
}
Dec 15, 2015 at 3:47 PM
Edited Dec 15, 2015 at 3:50 PM
thanks ! can you explain me why it was the problem?
i do this assigment at the end of the method .
Dec 15, 2015 at 4:24 PM
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] make sense since
0 < i0 <= a.Length ==> 0 <= (i0-1) < a.Length