Dafny是否支持元组解构语法？能否在function内使用解构？

方法（method）场景的解构 #

你给出的示例写法存在小问题，Dafny原生支持元组解构，但不支持提前单独声明变量后再做元组批量赋值，正确写法是将变量声明和解构绑定同时完成：

function method f(x:int) : (int,int) { (x,x+1) }

method test() {
    // 直接在解构时声明变量，可正常通过验证
    var (y, z) := f(1);
    assert y == 1 && z == 2;
}

如果只需要元组中的部分返回值，可以用下划线_作为通配符忽略不需要的字段，比如var (y, _) := f(1);就只会绑定第一个返回值到y。

function 内部的解构支持 #

function（包含function method）内部同样支持元组解构，由于function是表达式上下文，需要通过var/let绑定完成解构，不能使用语句式赋值，示例如下：

function g(x: int): int {
    // function内部直接通过var绑定解构元组
    var (a, b) := f(x);
    a * b
}

// 可通过验证：g(2) = 2 * 3 = 6
lemma VerifyG() {
    assert g(2) == 6;
}

注意事项 #

• 所有解构场景都要求变量声明与解构动作同步完成，暂不支持给已提前声明的变量做元组批量赋值。
• 该语法对任意长度的元组都生效，不局限于二元元组。

内容的提问来源于stack exchange，提问作者redjamjar