Spliting a list

Mar 26, 2014 at 8:37 AM
Please, could someone tell me why the following split method does not verify:
datatype List<T> = Nil | Cons(head:T, tail:List<T>)

function length<T> (xs:List<T>):int
    ensures length(xs) >= 0;
{
match xs
    case Nil => 0
    case Cons(_,t) => 1 + length(t)
}

function append<T> (xs:List<T>, ys:List<T>): List<T>
{
match xs
    case Nil => ys
    case Cons(h,t) => Cons(h,append(t,ys))
}

method split<T> (xs:List<T>) returns (pxs:List<T>,u:T)
    requires xs != Nil;
    ensures append(pxs,Cons(u,Nil)) == xs;
    // decreases length(xs);
{
    match xs 
    {
    case Cons(h,t) => { if (t == Nil)
                            { pxs,u := Nil,h ;}
                        else { 
                              var pt, u := split(t);
                              pxs := Cons(h,pt);
                              calc{ append(pxs,Cons(u,Nil));
                                    ==
                                    append(Cons(h,pt),Cons(u,Nil)) ; 
                                    ==
                                    Cons(h,append(pt,Cons(u,Nil)));
                                    == {assert append(pt,Cons(u,Nil))==t;} //Induction Hypothesis
                                    Cons(h,t);
                                    ==
                                    xs;
                                  }
                               }
                      }
    }
}
Thamks,
Paqui
Mar 26, 2014 at 12:10 PM
The problem is that the "else" branch introduces a new variable called u that shadows the out-parameter called u. In the calculation, you prove something about the value assigned to the local variable u, but this property does not hold of the out-parameter u (whose value is unknown). I think the confusion arises from the fact that the statement
var pt, u := split(t);
introduces both pt and u and then assigns these the two values returned by method split. To introduce only pt and then assign to both pt and u, you need two statements:
var pt;
pt, u := split(t);
With this change, your program verifies.

Rustan
Marked as answer by rustanleino on 3/26/2014 at 4:10 AM
Mar 26, 2014 at 12:15 PM
Ups! what a silly bug!
I was puzzled
Thanks,
Paqui