如何在Dafny中为相互递归函数定义一个减数？

问题描述

在“ Draft Dafny参考手册” 4.0.2中，它描述了为相互递归函数定义reduces子句，但是两个函数中递减的变量均为nat类型。我试图做同样的事情，但没有成功。区别在于变量不是同一类型。

datatype Trie = Trie(letters : map<char,Trie>,word : bool)

function  size(t:Trie) :(r:nat)
    decreases t 
  { 
      1 + sum_setT(t.letters.Values)
  }
function  sum_setT(xs: set<Trie>) : (z:nat) 
decreases xs
  {
    var working := xs; //Needed!
    if (|working| == 0) then 0
    else  (
        var x:Trie  :| x in working;
        var sofar:nat := sum_setT(working-{x});
        sofar + size(x)
    )   
  }

任何关于如何定义减少子句的想法都值得赞赏。

解决方法

如果两个函数（可能是同一个函数）递归调用，则需要显示每个调用以减少decreases函数给定的终止度量。更准确地说，如果在进入函数F时，decreases的{​​{1}}子句的计算结果为F，并且当X调用函数F时在G的{​​{1}}子句的值为G时，必须显示decreases超过Y。

“ exceeds”关系是一个内置的，有根据的顺序，但是您可以控制产生值X和Y的{​​{1}}子句。在您的示例中，定义它们的最简单方法是使用词典编组。在“外部”功能decreases中，使用X。在“内部”功能Y中，对同一size使用t。为了解决这个问题，您还需要向sum_setT添加t,xs作为参数。

在从t到t的通话中，sum_setT和size分别是sum_setT和X，这是因为按照Dafny的良好顺序，较短的Y元组会较大。

在t的递归调用中，t,t.letters.Values和decreases具有相同的第一成分（sum_setT），并且集合在X中严格较小。

在从Y返回到t的调用中，Y在结构上包含在sum_setT中，因此size超出了x需要。为了使验证者知道这一事实（即，让其知道参数t与t有某种关系），您需要向x添加一个前提条件。>

所以，最终的程序是

xs