如何让Dafny生成C#代码但不编译为.dll或.exe文件？

你之前使用/compile:0的问题在于，这个选项会完全禁用所有编译相关流程，包括C#代码生成环节，所以既没有二进制文件也没有.cs文件输出。要实现只生成C#代码、不编译为.dll/.exe的需求，需要使用正确的命令行选项组合：

针对旧版本Dafny（2.x系列） #

使用以下命令：

dafny /compileTarget:cs /compile:1 /noCompile your_file.dfy

• /compileTarget:cs：指定目标生成语言为C#
• /compile:1：启用编译流程（包含代码生成）
• /noCompile：在生成C#代码后终止流程，不执行后续的C#编译步骤（避免生成.dll/.exe）

针对新版本Dafny（3.x及以上） #

新版本提供了更直观的codegen子命令，直接生成目标语言代码，默认不会编译为二进制文件：

dafny codegen --lang cs your_file.dfy

如果需要跳过验证环节（加快代码生成速度），可以加上--no-verify：

dafny codegen --lang cs --no-verify your_file.dfy

还可以用--out指定代码输出目录：

dafny codegen --lang cs --out ./generated_code your_file.dfy

生成的C#文件会默认输出在与.dfy文件相同的目录下，文件名和源文件一致，后缀为.cs。

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