如何解决在验证终止时,如何告诉Dafny使用引理
Dafny利用reduces子句来验证递归函数是否终止。当验证失败时,可以以引理的形式给Dafny一个提示。在检查reduces子句实际减少时,如何告诉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,Node(v,rl,r))
case Node(v,Leaf,r) => Node(v,r)
}
function Leftheight(t:Twee) :(h:nat) decreases t
{
match t
case Leaf => 0
case Node(_,l,_) => 1+Leftheight(l)
}
lemma {:induction ll,r} decreasesHint(v:int,vl:int,ll:Twee,rl:Twee,r:Twee)
ensures Leftheight(Node(v,r)) ==
1+ Leftheight(Node(vl,r))) {}
function rotateallLeft(t:Twee) :Twee
decreases t,Leftheight(t)
{
match t
case Leaf => Leaf
case Node(v,rotateallLeft(r)) //decrases t
case Node(v,r) => //{ decreasesHint(v,vl,r);}
rotateallLeft(rotateLeft(Node(v,r)))
}
很抱歉,这么长的示例,但这是我第一次想提供检查终止的提示。错误failure to decrease termination measure
出现在最后一行rotateallLeft(rotateLeft(Node(v,r)
上。
解决方法
您可以从表达式内部调用引理。只需使用分号将引理调用与表达式的其余部分分开。
case Node(v,Node(vl,ll,rl),r) =>
decreasesHint(v,vl,rl,r);
rotateAllLeft(rotateLeft(Node(v,r)))
请注意,这不能完全解决您的终止问题,因为您的decreases
批注是t,Leftheight(t)
,这意味着递归调用必须减小t
或离开{ {1}}相同并减小左侧高度。但是,此递归调用不会使t
保持不变。我尝试将您的注释更改为仅t
,它接受了此decreases Leftheight(t)
,但在先前的case
上却给出了错误。也许您可以找到解决方法。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。