从Dafny调用C#时无法找到System.Net中的类型（.NET 6.0）

• Dafny默认编译生成的C#项目只引用核心基础类库，UdpClient、IPEndPoint所在的System.Net.Sockets属于网络扩展类库，不会被自动引入。而单独用dotnet编译C#文件时，控制台项目模板会自动包含这类常用库的引用，所以能正常编译。

• Dafny的C#代码生成逻辑不会自动添加对System.Net相关程序集的引用。普通dotnet项目会根据项目类型自动处理依赖，但Dafny编译时需要显式指定要引用的额外程序集。

• 若Dafny的extern声明里没明确关联对应程序集的信息，编译器也不会主动加载这类非核心的网络类库。

可行的解决方式 #

• 编译Dafny文件时，用--cs:reference参数显式指定引用的程序集：

  dafny compile --target:cs --cs:reference:System.Net.Sockets.dll YourDafnyFile.dfy
  

• 手动修改Dafny生成的C#项目文件，添加对System.Net.Sockets的引用，再用dotnet命令编译该项目。

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