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

Question

有什么办法来控制Dafny用于目标代码的命名约定？

是否可以在全局范围内使用符号常量？这样的事情：

? global const MaxValue = 10000; ? 

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

有什么办法将数值表达式转换为字符串？

Answer 1

是的，是的。

要控制Dafny在目标代码中使用的各种实体的名称，请使用{:extern "ThisIsTheNameIWant"}属性。大多数声明都支持该属性。例如，您可以将一个放在类上，另一个放在类中的方法上。有关更多示例，请参阅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 

Rustan