Dafny: cannot verify equational specification of a "length" function

Oct 31, 2012 at 4:53 PM
Edited Oct 31, 2012 at 11:53 PM

I'm working on some Dafny material for Haskell programmers and I've been toying with the idea of using equational specifications to relate Haskell to Dafny code.

However, I can't seem to get Dafny (or I guess Boogie/Z3) to solve the equational specification for the standard "length" function on lists.

The "length(Nil) == 0" case is fine, but "length(Cons(y, ys)) == 1 + length(ys)" ain't workin'.

 

datatype List<T> = Nil | Cons(T, List);

function length<T>(xs : List<T>) : nat
{
  match xs
  case Nil => 0
  case Cons(y, ys) => 1 + length(ys)
}

ghost method length_EqSpec()
  ensures length(Nil) == 0;
  ensures forall y, ys :: length(Cons(y, ys)) == 1 + length(ys); 
{
}