Dafny中provides机制是否在print语句中违规暴露变量值？

根据Dafny参考手册：“当名称以provides方式导出时，导入该名称的模块仅知晓名称，不知其声明细节”。

以下代码运行时验证器未报错：

module A { 
  export A provides a
  const a := 10;
}
module B {
  import opened Z = A`A
  method {:main} bValue() {
    //assert Z.a == 10;
    print Z.a,"\n"; 
  }
}

已知取消注释assert Z.a == 10后会报错，符合provides的定义，但为何验证器不对print Z.a报错？

原因解析 #

• provides导出规则的约束仅作用于Dafny的验证阶段：它限制导入模块在验证逻辑（比如断言、循环不变式、函数前置/后置条件等）中访问符号的具体声明细节（值、类型结构等），所以assert语句会因无法获取a的具体值而报错。
• print语句属于执行代码生成范畴：Dafny编译器处理print时，只需要确认符号的存在性（provides已经导出了a的名称，符号可见），不需要在验证阶段解析其具体值。实际执行时，编译器会从原模块A中获取a的实际值完成输出，因此不会触发验证错误。
• 本质上，provides的设计是为了隔离验证阶段的依赖，而非限制执行阶段的符号引用。

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