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

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

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

下面是证明各种简单定理的第一次尝试，在这种情况下是关于奇偶性的。达芙妮 /v. 1.9.9.40414/ 验证将 2 添加到偶数会产生偶数，但不接受任何已注释掉的条件。

由于我刚刚开始研究这个很棒的工具，我的方法或实现可能不正确。任何意见，将不胜感激。

有人能告诉我为什么这段代码会生成“索引越界”错误input[i*cols + j]吗？

我开始学习 Dafny，我刚刚学习了不变量。我有这个代码：

给定的错误如下：“这个循环不变量可能不会被循环维护。” 我想我可能需要另一个不变量，但我认为我的代码除此之外是正确的（我猜）。任何帮助表示赞赏。提前致谢。

他们来自微软，似乎他们是证明助理？除了语法上的差异之外，还有哪些实际方面使它们彼此不同（比如自动化能力、表达能力等）？我是形式验证的新手。

编辑：我不是在问哪个更好，我只是对这些工具提供的不同功能之间的技术比较感兴趣。我正在寻找这样的东西

将整数数组的负元素复制到另一个数组的方法具有以下属性：结果中的元素集是原始数组中元素的子集，在复制过程中保持不变。

下面代码中的问题是，只要我们在结果数组中写入一些内容，Dafny 就会不知何故忘记原始集合没有改变。如何解决这个问题？

编辑

按照James Wilcox 的回答，用序列上的谓词替换集合的包含是最有效的。

这是完整的规范（对于具有不同元素的数组）。后置条件必须在循环不变量中进行一些详细说明，并且在循环中间保留一个愚蠢的断言，但是所有幽灵变量都消失了，这很棒。

在以下将数组切片复制到另一个切片的代码中，表明源数组已保留的循环不变量未验证。

这与这个问题和另一个问题有关，但我还没有找到任何适用于这种情况的东西。

一些算法（分配二叉树......）需要计算以 2 为底的指数。如何为这种原生类型计算它？

这是一个明显的尝试：

它失败了，因为 Dafny 怀疑产品是否低于u32的最大值。如何证明它的值低于 2**10？

我在使用 VS 的 Dafny 插件时收到以下警告消息。谁能解释一下这是什么意思？

有问题的行是

另外，由于这只是一条警告消息，我是否可以断定验证是否成功？

我有一种方法会导致错误“验证不确定”。目前尚不清楚为什么验证是不确定的。似乎没有超时，也没有迹象表明哪些验证条件无法证明。简而言之：这是什么意思？

我使用的是 2.0.0 版。我不记得在 1.9.7 版本中看到此消息。

我遇到问题的特定方法是。