dafny - dafny 函数可以以与方法相同的方式返回两个东西吗？

Question

Although methods can return a pair consisting of two things (e.g. nats). Using a function I can only find how to return a single thing even if that is a pair (of nats).  This prevents me from using a single function to define a lexical decreases pair.

function twof() : (nat,nat) { (1,2)}
method twom() returns (r:  nat, r2: nat) { r,r2  := 5,6;} 

method Main() {
    var (x,y) := twof();
    //var x1,y1 := twof(); // Error
    var mx, my := twom();
}

这是 dafny 函数和方法之间的区别还是我错过了什么？

标签： dafny

Answer 1

正确的。Dafny 中的函数总是只返回一个值（但该值可以是一对）。方法可以有多个返回值。