Dafny 递归断言违规答案

【问题标题】：Dafny recursive assertion violationDafny 递归断言违规
【发布时间】：2017-11-03 23:15:47
【问题描述】：

我是 dafny 的新手，正在尝试让这段简单的代码工作。我想计算字符串中 char 的出现次数。我在第 4 行收到了一个断言违规。我知道我的函数正在查找正确数量的字符，但显然这个断言中有一些漏洞。在开始使用前置条件和后置条件之前，我试图了解基础知识，而没有它们应该是可能的。该函数只是检查字符串中的最后一个字符并返回 1 或 0，然后再次调用该函数，该函数会切断字符串的尾部，直到它为空。

method Main() {
  var s:string := "hello world";
  print tally(s, 'l');
  assert tally(s,'l') == 3;
}
function method tally(s: string, letter: char): nat
{
  if |s| == 0 then 0
  else if s[|s|-1] == letter then 1+tally(s[..|s|-1], letter)
  else 0 + tally(s[..|s|-1], letter)
}

http://rise4fun.com/Dafny/2lvt 这是我的代码的链接。

【问题讨论】：

标签： verification dafny

【解决方案1】：

自然会认为 Dafny 静态验证器可以评估任何代码，例如您的断言语句中的表达式。这验证器确实尝试评估这样的表达式，其中参数以常量形式给出（如您的"hello world"、'l'、和3)。但是，静态验证者希望避免递归永远（甚至递归太久），所以它并不总是完全通过这些表达式。在你的情况下，也有限制验证者能够对序列操作做什么。所以，在简而言之，尽管验证者试图提供帮助，但并不总是深入递归。

您可以通过两种方式绕过这些限制来获得验证者接受您的断言。

调试情况最可靠的方法是从较小的开始输入并建立到您正在使用的更长输入。这是相当然而，这很乏味，当达夫尼能够做到时，它会让你很感激这些东西是自动的。以下（验证）说明你会做什么：

var s := "hello world";
assert tally("he",'l') == 0;
assert tally("hel",'l') == 1;
assert "hell"[..3] == "hel";
assert tally("hell",'l') == 2;
assert "hello"[..4] == "hell";
assert tally("hello",'l') == 2;
assert "hello "[..5] == "hello";
assert tally("hello ",'l') == 2;
assert "hello w"[..6] == "hello ";
assert tally("hello w",'l') == 2;
assert "hello wo"[..7] == "hello w";
assert tally("hello wo",'l') == 2;
assert "hello wor"[..8] == "hello wo";
assert tally("hello wor",'l') == 2;
assert "hello worl"[..9] == "hello wor";
assert tally("hello worl",'l') == 3;
assert s[..10] == "hello worl";
assert tally(s,'l') == 3;

其实 Dafny 验证器没有扩展的东西（太多次）对你来说是“采取”操作（即表格s[..E])。以下中间断言也将验证自己并将有助于验证最终断言。这些中间断言显示验证者不认为做什么自动为您服务。

var s := "hello world";
assert "he"[..1] == "h";
assert "hel"[..2] == "he";
assert "hell"[..3] == "hel";
assert "hello"[..4] == "hell";
assert "hello "[..5] == "hello";
assert "hello w"[..6] == "hello ";
assert "hello wo"[..7] == "hello w";
assert "hello wor"[..8] == "hello wo";
assert "hello worl"[..9] == "hello wor";
assert s[..10] == "hello worl";
assert tally(s,'l') == 3;

您可能想知道，“我到底怎么会想出这个？”。这最系统的方法是从我上面的第一个例子开始。然后，您可以尝试修剪那里的许多断言，看看它是什么是验证者需要的。

（我现在想也许可以将 Dafny 验证器增强为也做这些操作。它可能会导致性能问题别处。我去看看。）

解决验证者限制的另一种方法是定义以不同的方式运行tally，特别是避免“采取” 操作，验证者不想扩展很多。它是不清楚要改变什么来让验证者对这些感到满意情况，或者如果这甚至可能的话，所以这个解决方法可能不是最好的。不过，我尝试了以下定义 tally 它使您的断言通过：

function method tally'(s: string, letter: char): nat
{
  tally_from(s, letter, 0)
}
function method tally_from(s: string, letter: char, start: nat): nat
  requires start <= |s|
  decreases |s| - start
{
  if start == |s| then 0
  else (if s[start] == letter then 1 else 0) + tally_from(s, letter, start+1)
}

请注意，这些定义不使用任何“take”操作。这里，验证者很乐意扩展所有递归调用，直到终于找到答案了。

鲁斯坦

【讨论】：