Dafny函数,while循环上的逻辑表达式无效 [英] Dafny function, invalid logical expression on while loop
问题描述
我是Dafny的新手,遇到了一些我无法弄清楚的错误。
I am new in Dafny and getting some errors that I can not figure it out.
- 在我的Dafny程序中,用于insertSort(< a href = https://rise4fun.com/Dafny/uj6 rel = nofollow noreferrer>代码在这里),我不明白为什么会得到
无效的逻辑表达式
上的While循环遍历变量i
。while(i< | input |)
- 在交换部分的同一代码中(
input [ j:= b]; input [j-1:= a];
)我也得到预期方法调用,找到表达式
。根据教程input [j:= b]
将seq输入的索引j替换为b
- in my Dafny program for insertionSort (the code is here), I do not understand why I get an
invalid logical expression
on While loop over variablei
.while (i < |input|)
- in the same code at the swapping part (
input[j := b]; input[j-1 := a];
) also I getexpected method call, found expression
. According to the tutorialinput[j:=b]
is replacing index j of seq input with the value of b
推荐答案
第一个错误是因为您被声明为函数
而不是方法
。在Dafny中,函数
的主体应为表达式,而不是语句序列。因此,当解析器看到关键字 while时,它就意识到出了点问题(因为 while不能成为语句的一部分)并给出了错误消息。我不确定为什么错误消息引用的是逻辑表达式。
The first error is because you are declared a function
rather than a method
. In Dafny the body of a function
is expected to be an expression, not a sequence of statements. So when the parser sees the keyword "while", it realizes something is wrong (since "while" can't be part of a statement) and gives an error message. I'm not sure why the error message refers to a "logical" expression.
无论如何,您可以通过声明方法
而不是函数
。
Anyway, you can fix this problem by declaring a method
rather than a function
.
您需要一种方法,因为您使用的是命令式算法而不是功能性算法。确实,您需要一个子例程,该子例程根据其输入来计算其输出而没有副作用。但是,在Dafny中,当您要使用的方法涉及诸如赋值和while循环之类的命令式构造时,您仍然会使用方法
。
You need a method because you are using an imperative algorithm and not a functional algorithm. It's true that you want a subroutine that computes its output as a function of its input with no side effects. But, in Dafny, you still use a method
for this when the way you want to do it involves imperative constructs like assignments and while loops.
第二个问题是 input [j:= b]
是一个表达式,而解析器期望一份声明。您可以通过重写 input [j:= b];来解决此问题。 input [j-1:= a];
作为 input:= input [j:= b];输入:=输入[j-1];
。
The second problem is that input[j := b]
is an expression whereas the parser exepected a statement. You can fix this by rewriting input[j := b]; input[j-1 := a];
as input := input[j:=b]; input := input[j-1];
.
不幸的是,这将导致另一个问题是,在Dafny中无法分配输入参数。因此,您最好创建另一个变量。
Unfortunately, that will lead to another problem, which is that, in Dafny, input parameters can't be assigned to. So you are better off making another variable. See below, for how I did that.
method insertionSort(input:seq<int>)
// The next line declares a variable you can assign to.
// It also declares that the final value of this variable is the result
// of the method.
returns( output : seq<int> )
// No reads clause is needed.
requires |input|>0
// In the following I changed "input" to "output" a few places
ensures perm(output,old(input))
ensures sortedBetween(output, 0, |output|) // 0 to input.Length = whole input
{
output := input ;
// From here on I changed your "input" to "output" most places
var i := 1;
while (i < |output|)
invariant perm(output,old(input))
invariant 1 <= i <= |output|
invariant sortedBetween(output, 0, i)
decreases |output|-i
{
...
output := output[j := b];
output := output[j-1 := a];
j := j-1;
...
}
}
由于无法更改输入参数,因此无论您在何处使用 old(input)
,都可以使用 input
。他们是同一回事。
By the way, since input parameters can't be changed, wherever you have old(input)
, you could just use input
. They mean the same thing.
这篇关于Dafny函数,while循环上的逻辑表达式无效的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!