Dafny递归断言冲突

Question

我是达夫尼的新手，我正试图让这段简单的代码开始工作。我想要计数字符在字符串中的出现情况。我在第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这里是我的代码的链接。

Answer 1

认为Dafny静态验证器可以计算任何代码是很自然的，就像assert语句中的表达式。验证器确实尝试计算像这样的表达式，其中参数作为常量给出(比如"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;

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

(我现在在想，也许达夫尼验证器也可以做这些操作。它可能会在其他地方造成性能问题。我来看看。)

另一种绕过验证器限制的方法是以不同的方式定义函数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)
}

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

鲁斯坦