为什么达夫尼抱怨这个职位条件“确保ListMap(x => x+ 1，Cons(1，Cons(2，Nil) == Cons(2，Cons(3，Nil))，以及它如何被修复？

Question

function method ListMap<T,X>(f : (T -> X), l : List<T>) : List<X>
    ensures ListMap(x => x + 1, Cons(1, Cons(2, Nil))) == Cons(2, Cons(3, Nil))
{
    match l {
        case Nil => Nil
        case Cons(n, l') => Cons(f(n), ListMap(f, l'))
    }
}

达芙妮在这里提出了两项控诉。

关于"case Nil“的

1. ：一个后置条件可能在此返回路径上不保持。
2. 关于”确保.“：该后置条件可能不保持返回路径。

这个片段来自于“用Dafny语言介绍软件验证:验证程序正确性”一书，但是我找不到它的Errata。

Answer 1

这里有两件事您可以马上解决：

如果计算(在假想的鬼环境中)，确保不会终止，因为您将其作为一个内在的后置条件提供，因此您将陷入麻烦。Dafny可以确保当前函数的输出，但是对于函数本身的所有其他调用，它必须证明终止。

您提供的是一个后置条件的示例，而不是ListMap函数的每个用户都应该知道的事实。

解决方案是在引理中重构您的确保：

datatype List<T> = Nil | Cons(t: T, tail: List<T>)

function method ListMap<T,X>(f : (T -> X), l : List<T>) : List<X>
{
    match l {
        case Nil => Nil
        case Cons(n, l') => Cons(f(n), ListMap(f, l'))
    }
}

lemma ListMapExample()
  ensures ListMap(x => x + 1, Cons(1, Cons(2, Nil))) == Cons(2, Cons(3, Nil))
{
}