为元组解构语法？

Question

因此，我想知道在Dafny中是否有任何对析构语法的支持。大致如下的内容：

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

method test() {
    var y:int;
    var z:int;
    (y,z) := f(1);
}

事实上，我想更进一步，因为我想在function中进行重构。

Answer 1

根据参考手册，您不能对赋值语句执行此操作，而只能对变量声明语句执行此操作，如下所示：

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

method test() {
    var (y,z) := f(1);
}

如果您想注释这些类型，可以这样做：

var (y:int, z:int) := f(1);

您还可以使用let表达式在函数中执行此操作，如下所示：

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

function g() {
    var (y,z) := f(1);
    y+z
}