如何解决Dafny实现Cantor配对函数时报invalid LogicalExpression错误的问题

开发者阿泽

2026-10-1

Dafny Cantor逆配对函数报错修复方案

问题根因

你遇到的invalid LogicalExpression报错有两个核心原因：

你使用:|（such that）绑定变量x、y时，Dafny无法自动证明对任意自然数n，满足n == (x+y)*(x+y+1)/2 + y的x、y一定存在，因此不允许直接返回这组未被证明存在的变量。
function method要求逻辑可执行，你使用的非构造性定义没有给出明确的计算步骤，无法生成可运行的代码，因此触发了逻辑校验错误。

修复方案

使用Cantor逆配对函数的标准构造性实现替换原有非构造式定义，代码如下：

// 辅助函数：计算自然数的整数平方根，满足返回值s为最大的s*s <=n的自然数
function method sqrt_nat(n: nat): nat
  ensures sqrt_nat(n) * sqrt_nat(n) <= n < (sqrt_nat(n) + 1) * (sqrt_nat(n) + 1)
{
  if n == 0 then 0
  else var s := sqrt_nat(n / 4);
  if (2*s + 1) * (2*s + 1) <= n then 2*s + 1 else 2*s
}

function method unpair(n: nat): (x: nat, y: nat)
  ensures n == (x + y) * (x + y + 1) / 2 + y
{
  var s := sqrt_nat(8 * n + 1);
  s := (s - 1) / 2;
  y := n - s * (s + 1) / 2;
  x := s - y;
  (x, y)
}