你如何告诉 Dafny 在验证终止时使用引理答案

【问题标题】：How do you tell Dafny to use a lemma when validating termination你如何告诉 Dafny 在验证终止时使用引理
【发布时间】：2020-09-21 02:34:58
【问题描述】：

Dafny 使用减少子句来验证递归函数是否终止。当验证失败时，可以给 Dafny 一个提示，在这种情况下是以引理的形式。在检查减少子句是否实际减少时，如何告诉 Dafny 使用引理？

datatype List<T> = Nil | Cons(head:T, tail:List<T>) 
datatype Twee = Node(value : int, left : Twee, right : Twee) | Leaf
function rotateLeft(t:Twee) :Twee
{
    match t 
       case Leaf => t 
       case Node(v,Node(vl,ll,rl),r) => Node(vl,ll,Node(v,rl,r))
       case Node(v,Leaf,r) => Node(v,Leaf,r)
}
  function Leftheight(t:Twee) :(h:nat) decreases t
{
  match t 
    case Leaf => 0 
    case Node(_,l,_) =>  1+Leftheight(l)
}     
lemma {:induction ll, rl, r} decreasesHint(v:int, vl:int, ll:Twee,rl:Twee,r:Twee)
   ensures   Leftheight(Node(v,Node(vl,ll,rl),r)) == 
           1+ Leftheight(Node(vl,ll, Node(v,rl,r)))  {} 
function rotateAllLeft(t:Twee) :Twee
    decreases t, Leftheight(t)
{
    match t 
       case Leaf => Leaf 
       case Node(v,Leaf,r) => Node(v,Leaf,rotateAllLeft(r))  //decrases t
       case Node(v,Node(vl,ll,rl),r) => //{ decreasesHint(v,vl,ll,rl,r);}
                  rotateAllLeft(rotateLeft(Node(v,Node(vl,ll,rl),r)))     
}

对不起，这么长的例子，但这是我第一次想给出检查终止的提示。错误failure to decrease termination measure出现在最后一行rotateAllLeft(rotateLeft(Node(v,Node(vl,ll,rl),r)。

【问题讨论】：

标签： terminate hint dafny

【解决方案1】：

您可以从表达式内部调用引理。只需使用分号将引理调用与表达式的其余部分分开即可。

      case Node(v,Node(vl,ll,rl),r) =>
        decreasesHint(v,vl,ll,rl,r);
        rotateAllLeft(rotateLeft(Node(v,Node(vl,ll,rl),r)))

请注意，这并不能完全解决您的终止问题，因为您的 decreases 注释是 t, Leftheight(t)，这意味着递归调用必须要么使 t 更小，要么使 t 保持不变 em> 并使左侧高度更小。但是这个递归调用不会让t 保持不变。我尝试将您的注释更改为仅decreases Leftheight(t)，它接受了这个case，但在之前的case 上给出了错误。也许您可以找到解决方法。

【讨论】：

非常感谢我曾尝试在那里添加它，但也添加了 { .. }。