问题标签 [dafny]

我怎样才能写一个function接受一个整数序列并返回一个对序列的 dafny？例如，输入 = [1,2]，输出 = [Pair(1,1), Pair(1,2)]

我从

这似乎不起作用。

我想知道我需要在以下内容中添加什么以使其通过 dafny？

I am struggling with dafny syntax.

searchAndReplace receives three arrays of chars. Let's imagine line is [s][n][a][k][e]; pat is [n][a] and dst is [h][i]. I want to search for all the occurrences of pat in line and replace it with dst resulting in [s][h][i][k][e]

Method findwill return the indice of the first letter in line that is equal to pat.

Method deletewill remove pat from line at the variable at returned at find, and move all the others elements after at+p to the left in order to fill the null spaces.

Method insertwill make space in order to dst be added to lineat atby moving all the characters between atand at + p ppositions to the right.

I created an auxiliar function which will compare patand dst in order to verify that they aren't equal(if they were it would be replacing infinitely time dstin line in case patexisted in line) For now i'm receiving the error "then expected" on the following section of code inside function checkIfEqual:

The full code:

我正在编写一个使用查找、删除和插入方法的搜索和替换方法。我在 while 循环中调用这三个方法，但我不确定应该使用哪些前置条件。

完整代码：

更新

解决一些愚蠢问题的问题，下面用给定的类和相应的方法进行描述。如果您需要其他东西，请告诉我，提前谢谢。此外，该链接已使用rise4fun 中的所有这些代码进行更新。

在rise4fun

我正在尝试在 dafny 中创建一个谓词，以确定字符数组是否包含任何重复项。它最终应该测试以下内容：对于数组中的任何两个元素，如果 theor 值相等，则它们的索引也必须相等。请忽略少于2个元素的情况

但是，当我运行以下测试时，断言失败。为什么会这样？

我正在尝试验证一个将凯撒密码应用于字符串的程序。必须返回原始字符串

更新字符串值的最佳方法是什么，类似于：

我正在使用 dafny 来证明对数字列表求和的不变量：

dafny 无法验证这一点。我错过了作为后置条件sum吗？

Dafny 谓词怎么可能既不真也不假？

这个：

产生双重断言违规：

给定以下公理：

N1==A我们想用 Dafny来证明这一点。

我尝试过遵循 Dafny 程序：

但达夫尼未能证明这一点。有没有办法N1==A从给定的公理？