控制 Dafny 命名约定和使用常量

Question

有什么方法可以控制 Dafny 用于目标代码的命名约定吗？

是否可以全局使用符号常量？像这样：

? global const MaxValue = 10000; ?

method Method1 (a : int) returns (b : int)
  requires a < MaxValue

有什么方法可以将数值表达式转换为字符串吗？

Answer 1

是的，是的。

要控制 Dafny 在目标代码中使用的各种实体的名称，请使用 {:extern "ThisIsTheNameIWant"} 属性。大多数声明都支持此属性。例如，您可以将一个放在 class 上，将另一个放在 class 内的方法上。有关更多示例，请参阅 Dafny 测试套件中的 Test/dafny0/Extern.dfy 文件。如果您想查看生成的内容，请使用命令行中的 /spillTargetCode:1 标志。

对于常量，使用：

const MaxValue := 10000

（请注意，直到最近，您还必须明确提供常量类型，因此您必须编写

const MaxValue: int := 10000

如果您从源构建最新版本的 Dafny，则类型是从右侧表达式推断出来的。）

从 Ada 语言中借用的一个绝妙功能是，您可以在数字文字中的任意两个数字之间插入下划线。如果你使用大字面量，其中有一堆零，那么这会让你的眼睛更容易看到你写了正确的数字。例如：

const MaxValue := 10_000
const PhoneNumber := 512_555_1212
const SignedInt32Limit := 0x8000_0000

鲁斯坦

控制 Dafny 命名约定和使用常量

Controlling Dafny naming convention and using constants

dafny