dafny函数可以以与方法相同的方式返回两件事吗？

问题描述

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中的函数总是精确地返回一个值（但该值可以是一对）。方法可以有多个返回值。