为何Dafny允许未初始化返回结果？如何强制校验返回值赋值？

你遇到的是Dafny的默认初始化行为：对于归纳类型（比如你定义的Results）、数值类型、引用类型等，未显式赋值的返回参数会被自动赋予该类型的默认值——归纳类型取第一个构造函数（这里就是Foo），数值类型取0，引用类型取null。这就是为什么你的代码能通过验证且返回Foo。

要让Dafny强制校验返回结果必须在返回前被显式赋值，有两种方式：

单个方法级别 #

给目标方法添加{:initialize "strict"}属性，仅对该方法启用严格初始化检查：

datatype Results = Foo | Bar

{:initialize "strict"}
method test() returns (r:Result)
{
    // 若不添加 r := Foo; 这样的赋值语句，Dafny会报错：未初始化的返回参数r
    r := Foo;
}

全局级别 #

使用Dafny命令行参数--initialize:strict，让所有方法、局部变量都遵循严格初始化规则，任何未显式赋值的变量（包括返回参数）都会触发验证错误。

这个严格模式下，不仅返回参数，方法内的局部变量也必须先赋值再使用，完全消除了默认值自动填充的行为，更贴近C/C++等语言的初始化校验逻辑。

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