Dafny 递归断言违规

Question

我是 dafny 的新手，正在尝试让这段简单的代码工作。我想计算字符串中 char 的出现次数。我在第 4 行收到断言违规。我知道我的函数正在查找正确数量的字符，但显然此断言中存在一些漏洞。在开始使用 pre 和 post 条件之前，我试图了解基础知识，而没有它们应该是可能的。该函数简单地检查字符串中的最后一个字符和 returns 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 这是我的代码的 link。

Answer 1

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

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

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

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验证器没有展开的东西（太多了次）对你来说是 "take" 操作（即表达式形式 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;

您可能想知道，"how in the world would I come up with this?"。这最系统的方法是像我上面的第一个例子一样开始。然后，您可以尝试修剪那里的许多断言，看看它是什么是验证者的需求。

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

绕过验证器限制的另一种方法是定义以不同的方式运行 tally，特别是避免 "take" 操作，验证者不想扩展太多。这是不清楚要更改哪些内容才能使验证者满意情况，或者如果这完全可能，那么这个解决方法可能不是最好的。不过，我尝试了以下定义 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" 操作。这里，验证者很乐意扩展所有递归调用，直到找到最终答案。

鲁斯坦

Dafny 递归断言违规

Dafny recursive assertion violation

verification

dafny