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[i1..] + [a[i1]];
assert a[i] <= 0 ==> p0 == RecursivePositiveProduct(a,i1) && a[i] > 0 ==> a[i]*p0 == RecursivePositiveProduct(a,i1) ;
// Alternation (4.1)
if {
case(a[i] > 0) =>
p := p0 * a[i];
case (a[i] <= 0) =>
// Skip command (3.2)
}
assert a[i..] == a[i1..] + [a[i1]] && 0 <= i1 <=a.Length &&
p == RecursivePositiveProduct(a,i) && 0 <= (i1) < i;
//followiong assignment (3.5)
i := i  1;
assert 0 <= i <=a.Length && p == RecursivePositiveProduct(a,i) && 0 <= i < i0;
}
THANKS!



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[i1..] + [a[i1]] could ever be true. Perhaps I am confused, but I think that the slice
a[i..] is one element smaller than the slice a[i1..] so the sequence
a[i1..] + [a[i1]] 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 ==i01 && 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



I think that it should be p, i := p0, i01;
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.Lengthfrom
{
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 .



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[i01] make sense since
0 < i0 <= a.Length ==> 0 <= (i01) < a.Length

