(Dafny)过滤元音时，后置条件可能不成立

Question

我正在为我的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

Answer 1

只有dafny可以在filterTheVowels中用于验证countTheVowels返回值的信息大于0。它不连接元音数量和计数之间的点，因为它不是后置条件的一部分。避免这种情况的一种方法是使countTheVowels函数方法成为

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..])
}