1

我是 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 这是我的代码的链接。

4

1 回答 1

1

很自然地认为 Dafny 静态验证器可以评估任何代码，例如您的断言语句中的表达式。验证器确实会尝试评估像这样的表达式，其中参数作为常量给出（例如 your "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”操作（即 form 的表达式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)
}

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

鲁斯坦

于 2017-06-06T01:43:06.597 回答