0

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

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

? global const MaxValue = 10000; ?

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

有没有办法将数字表达式转换为字符串？

4

1 回答 1

2

是的，是的。

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

对于常量，使用：

const MaxValue := 10000

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

const MaxValue: int := 10000

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

从 Ada 语言中借用的一个漂亮特性是，您可以在数字文字的任意两位数字之间插入下划线。如果您使用包含一堆零的大型文字，那么这会让您的眼睛更容易看到您写的数字是正确的。例如：

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

鲁斯坦

于 2017-07-25T01:36:56.560 回答