0

我正在为我的 Dafny 考试而学习，但我不知道我的代码有什么问题。

我认为这与我的“索引超出范围”错误有关，但我不知道如何解决。

任何提示将不胜感激。

问题：

Given an array of characters, it filters all the vowels.

我的做法：

method filterTheVowels(a: array<char>) returns (vowels: array<char>)
requires a.Length > 0
ensures forall i, j | 0 <= i < a.Length && 0 <= j < vowels.Length :: a[i] in ['a','e','i','o','u'] ==> vowels[j] in ['a','e','i','o','u']
// ^^^ THE POSTCONDITION THAT MIGHT NOT HOLD ^^^
{
    var count := countTheVowels(a);
    vowels := new char[count];
    var i := 0;
    var j := 0;
    while i < a.Length
    invariant 0 <= i <= a.Length
    invariant 0 <= j <= count
    invariant forall k, l | 0 <= k < a.Length && 0 <= l < j :: a[k] in ['a','e','i','o','u'] ==> vowels[l] in ['a','e','i','o','u']
    {
        if a[i] in ['a','e','i','o','u'] {
            vowels[j] := a[i]; // INDEX OUT OF RANGE
            j := j + 1;
        }
        i := i + 1;
    }
}

辅助方法：

method countTheVowels(a: array<char>) returns (count: int)
requires a.Length > 0
ensures count >= 0
{
    count := 0;
    var i := 0;
    while i < a.Length
    invariant 0 <= i <= a.Length
    {
        if a[i] in ['a','e','i','o','u'] {
            count := count + 1;
        }
        i := i + 1;
    }
}

method Main()
{
    var a := new char[6];
    a[0],a[1],a[2],a[3],a[4],a[5] := 'c','h','e','e','s','e';
    var e := countTheVowels(a);
    print e;
}

产生的错误：

/home/dafny/exam/fclex.dfy(9,1): Error: A postcondition might not hold on this return path.
/home/dafny/exam/fclex.dfy(3,8): Related location: This is the postcondition that might not hold.
/home/dafny/exam/fclex.dfy(3,113): Related location
Execution trace:
    (0,0): anon0
    /home/dafny/exam/fclex.dfy(9,2): anon24_LoopHead
    (0,0): anon24_LoopBody
    /home/dafny/exam/fclex.dfy(9,2): anon25_Else
    (0,0): anon35_Then
/home/dafny/exam/fclex.dfy(15,9): Error: index out of range
Execution trace:
    (0,0): anon0
    /home/dafny/exam/fclex.dfy(9,2): anon24_LoopHead
    (0,0): anon24_LoopBody
    /home/dafny/exam/fclex.dfy(9,2): anon25_Else
    /home/dafny/exam/fclex.dfy(9,2): anon35_Else
    (0,0): anon36_Then

Dafny program verifier finished with 4 verified, 2 errors
4

1 回答 1

0

关于返回值的唯一信息dafny可以用于验证是否大于 0。它不连接元音数量和计数之间的点，因为它不是后置条件的一部分。避免这种情况的一种方法是制作函数方法filterTheVowelscountTheVowelscountTheVowels

function method countTheVowels(a: seq<char>) : int
{
  if |a| == 0 then 0
  else if a[0] in ['a','e','i','o','u'] then 1 + countTheVowels(a[1..])
  else countTheVowels(a[1..])
}
于 2021-12-11T16:45:30.260 回答