
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



The problem is that the "else" branch introduces a new variable called
u that shadows the outparameter 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 outparameter 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



Ups! what a silly bug!
I was puzzled
Thanks,
Paqui

