1

在“Draft Dafny 参考手册”4.0.2 中，它描述了为相互递归函数定义减少子句，但两个函数中减少的变量都是类型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)
    )   
  }

任何想法如何定义减少子句都非常感谢。

4

1 回答 1

1

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

“超出”关系是一个内置的有根据的顺序，但您可以控制decreases产生值X和的子句Y。在您的示例中，定义这些的最简单方法是使用字典元组。在“外部”函数中size，使用t. 在“内部”功能中，sum_setT,t, xs用于相同的t. 要解决这个问题，您还需要将其添加t为参数sum_setT。

在 from sizeto sum_setT, Xand Yare tand的调用中t, t.letters.Values，它更小，因为 Dafny 中内置的有根据的顺序认为更短的decreases元组更大。

在 的递归调用中sum_setT，X和Y具有相同的第一个组件 ( t) 并且集合严格小于Y.

在从sum_setTback 到的调用中size，该值x在结构上包含在 中t，因此根据需要t超出x。为了让验证者知道这个事实（也就是说，让它知道参数xs与 有某种关系t），您需要在sum_setT.

所以，最终的程序是

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

function size(t: Trie): nat
  decreases t
{ 
  1 + sum_setT(t, t.letters.Values)
}

function sum_setT(t: Trie, xs: set<Trie>): nat
  requires xs <= t.letters.Values
  decreases t, xs
{
  if |xs| == 0 then
    0
  else
    var x :| x in xs;
    var sofar := sum_setT(t, xs - {x});
    sofar + size(x)
}
于 2020-09-16T18:27:43.667 回答