如何在Dafny中形式化规范并验证等价于JavaScript原生split方法的字符串分割函数

Hey there! 你遇到的问题在Dafny开发里太常见了：就算你的函数功能上完全正确，但如果不给它精确的形式化规范，Dafny根本没法帮你验证断言。你一开始想到的那些性质方向是对的，但需要细化到完全匹配JavaScript原生split的行为，还要把这些规范附加到函数上，让Dafny能跟踪递归过程中的不变量。

咱们一步步来解决这个问题：

第一步：把JavaScript Split的核心行为转化为Dafny规范 #

首先得明确JS原生split的所有关键行为，再把这些行为翻译成Dafny能理解的谓词和函数：

1. 完整性：分割结果能还原原字符串

用分割结果加上分隔符拼接起来，必须和原字符串完全一致。你写的sumSeq函数几乎完美，只要把它标记为ghost函数（因为只用于规范，不参与执行），再把这个性质作为后置条件即可。

2. 分割片段不含分隔符（特殊情况例外）

如果分隔符非空，每个分割出来的片段里不能包含分隔符；如果分隔符是空字符串，每个片段必须是单个字符（因为JS会把字符串拆成单个字符）。我们可以用一个谓词来定义这个规则：

ghost predicate NoSeparatorInPart(part: string, separator: string) {
  if |separator| == 0 then
    |part| == 1  // 空分隔符要求每个片段都是单个字符
  else
    // 非空分隔符：片段中不存在分隔符子串
    !(exists i: nat :: i + |separator| <= |part| && part[i..i+|separator|] == separator)
}

3. 正确覆盖原字符串并保持顺序

分割出来的片段必须是原字符串连续且不重叠的子串，分隔符必须恰好出现在两个片段之间（包括开头、结尾的分隔符，以及连续分隔符的情况）。用递归谓词来表达这个逻辑最合适：

ghost predicate CoversString(parts: seq<string>, s: string, separator: string) {
  if |parts| == 0 then
    s == "" && separator == ""  // JS中split("", "")返回空序列
  else if |parts| == 1 then
    parts[0] == s  // 没有找到分隔符，直接返回原字符串
  else
    // 第一个片段是前缀，后面跟着分隔符，剩余片段覆盖原字符串的剩余部分
    exists pos: nat :: 
      pos == |parts[0]| + |separator| && 
      pos <= |s| && 
      s[0..|parts[0]|] == parts[0] && 
      s[|parts[0]|..pos] == separator && 
      CoversString(parts[1..], s[pos..], separator)
}

第二步：给函数附加规范 #

现在要把这些不变量作为后置条件加到split和splitHelper上。对于splitHelper，还需要前置条件来描述递归过程中保持的不变量：

带规范的splitHelper函数

function splitHelper(s: string, separator: string, index: nat, sindex: nat, results: seq<string>): seq<string>
  requires index <= |s|
  requires sindex <= |s|
  requires sindex <= index
  // 不变量：已生成的结果加上当前未完成片段等于原字符串的前index部分
  requires sumSeq(results, separator) + s[sindex..index] == s[0..index]
  // 不变量：已生成的所有片段都不含分隔符
  requires forall i: nat :: i < |results| ==> NoSeparatorInPart(results[i], separator)
  // 不变量：当前未完成片段不含分隔符（分隔符非空时）
  requires |separator| > 0 ==> !(exists i: nat :: i + |separator| <= index - sindex && s[sindex + i .. sindex + i + |separator|] == separator)
  decreases |s| - index
  // 最终结果满足所有核心不变量
  ensures sumSeq(splitHelper(s, separator, index, sindex, results), separator) == s
  ensures CoversString(splitHelper(s, separator, index, sindex, results), s, separator)
  ensures forall i: nat :: i < |splitHelper(s, separator, index, sindex, results)| ==> NoSeparatorInPart(splitHelper(s, separator, index, sindex, results)[i], separator)
{
  if index >= |s| then results + [s[sindex..index]]
  else if |separator| == 0 && index == |s|-1 then splitHelper(s, separator, index+1, index, results)
  else if |separator| == 0 then splitHelper(s, separator, index+1, index+1, results + [s[sindex..index]])
  else if index+|separator| > |s| then splitHelper(s, separator, |s|, sindex, results)
  else if s[index..index+|separator|] == separator then splitHelper(s, separator, index+|separator|, index+|separator|, results + [s[sindex..index]])
  else splitHelper(s, separator, index+1, sindex, results)
}

带规范的split函数

ghost function sumSeq(ss: seq<string>, separator: string): string {
  if |ss| == 0 then ""
  else if |ss| == 1 then ss[0]
  else ss[0] + separator + sumSeq(ss[1..], separator)
}

function split(s: string, separator: string): seq<string>
  ensures sumSeq(split(s, separator), separator) == s
  ensures CoversString(split(s, separator), s, separator)
  ensures forall i: nat :: i < |split(s, separator)| ==> NoSeparatorInPart(split(s, separator)[i], separator)
  // 显式声明边缘情况，让验证更清晰
  ensures separator == "" ==> (|split(s, separator)| == |s| && forall i: nat :: i < |s| ==> split(s, separator)[i] == s[i..i+1])
  ensures |separator| > |s| ==> split(s, separator) == [s]
{
  splitHelper(s, separator, 0, 0, [])
}

第三步：验证你的断言 #

有了这些规范之后，Dafny就能验证你在Main方法里的断言了。比如：

method Main() {
  var example := split("a,bc", ",");
  assert example == ["a", "bc"];  // 现在可以成功验证！
  
  // 测试边缘情况
  assert split("", "") == [];
  assert split("", ",") == [""];
  assert split("||", "||") == ["", ""];
  assert split("||", "|") == ["", "", ""];
}

为什么这样能行？ #

通过添加前置条件和后置条件，你给了Dafny足够的逻辑规则，让它能证明每一步递归都保持了不变量，最终结果完全符合JavaScript split的行为。关键就是把JS split的 informal 规则转化成了机器能检查的精确逻辑。

额外提示 #

• 一定要测试所有边缘情况（空字符串、空分隔符、分隔符比字符串长、连续分隔符等），这些地方最容易出现bug或者验证漏洞。
• CoversString谓词正确处理了分隔符的位置和顺序，这对验证分割位置的正确性至关重要。

备注：内容来源于stack exchange，提问作者Hath995