CODEWITHSUNDEEP
dafny
gel
gel

Reputation: 301

Why does Dafny think there might be a problem with this precondition when using a ghost variable?

Let's say I have the following class:

class Testing {
    ghost var myGhostVar: int;

    method Init() 
    modifies this
    ensures this.myGhostVar == -1    
    {
        this.myGhostVar := -1;
        assert this.myGhostVar == -1;
    }


    method MyTestingMethod(list: array<int>, t: int)
    modifies this
    requires list.Length > 1
    requires this.myGhostVar == -1
    requires t == -1
    ensures MyPredicate(list, myGhostVar)
    ensures this.myGhostVar < list.Length
    {
        this.Init();
        assert this.myGhostVar < 0;
        assert list.Length > 0;
        assert this.myGhostVar < list.Length;
    }

    predicate MyPredicate(list: array<int>, startIndex: int)
    requires startIndex < list.Length
    {
        true
    }
}

For some reason, Dafny say that the call to MyPredicate(...) might not hold. But if I instead use t as the argument instead of myGhostVar; Dafny has no complaints.

Both have the same requires predicate which makes it all a bit confusing. Is it something that I am missing when using ghost variables?

Upvotes: 0

Views: 1379

Answers (1)

smithjonesjr
smithjonesjr

Reputation: 981

It's not an issue with ghost variables - you could check and see that you'd have the same issue if you removed the ghost keyword.

The issue is that to call MyPredicate(list, myGhostVar), you need to satisfy the pre-condition, which here would be myGhostVar < list.Length.

You actually have this condition in your ensures clause, which is great!

    ensures MyPredicate(list, myGhostVar)
    ensures this.myGhostVar < list.Length

But your call to MyPredicate is before the condition you need. Try flipping around the order:

    ensures this.myGhostVar < list.Length
    ensures MyPredicate(list, myGhostVar)

And you should see that Dafny stops complaining.

In general, Dafny will try to prove that the pre-conditions within an ensures clauses hold using the previous ensures clauses.

Both have the same requires predicate which makes it all a bit confusing. Is it something that I am missing when using ghost variables?

Here, I think you're asking about the clauses

    requires this.myGhostVar == -1
    requires t == -1

and wondering why it can't use the this.myGhostVar == -1 pre-condition to prove this.myGhostVar < list.Length.

The answer is that the this.myGhostVar == -1 is a pre-condition, meaning Dafny knows that it holds on entry, but the value of this.myGhostVar might change during the execution of the method. So that doesn't help Dafny when checking the post-condition.

Note that Dafny doesn't look at the body of its methods when checking the well-formedness of its post-conditions. For that purpose, Dafny only knows what you tell it in the method signature.

Upvotes: 2

Related Questions