CODEWITHSUNDEEP
arraysdafnypost-conditions
Irfan Zainudin
Irfan Zainudin

Reputation: 65

(Dafny) Postcondition might not hold when filtering vowels

I'm studying for my Dafny exam and I don't know what's wrong with my code.

I think it has something to do with my "index out of range" error but I don't know how to solve that.

Any hints would be greatly appreciated.

The problem:

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

My approach:

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;
    }
}

The auxiliary methods:

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;
}

The errors produced:

/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

Upvotes: 0

Views: 118

Answers (1)

Divyanshu Ranjan
Divyanshu Ranjan

Reputation: 1625

Only information dafny can use for verification in filterTheVowels about countTheVowels return value is it is greater than 0. It does n't connect dot between number of vowels and count as it is not part of post condition. One way to avoid this is to make countTheVowels function method

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

Upvotes: 0

Related Questions