CODEWITHSUNDEEP
dafny
Andrici Cezar
Andrici Cezar

Reputation: 603

Assertion fails after modifying another array in Dafny

I ran into a weird problem in Dafny. I tried to extract it as much as possible here: https://rise4fun.com/Dafny/F7sK

The thing is, after the modification of truthAssignment, stack.valid fails even if stack.valid doesn't know about truthAssignment. 

assert stack.valid();
truthAssignment[variable] := 1;
assert stack.valid();  // assertion violation

Upvotes: 1

Views: 148

Answers (2)

Rustan Leino
Rustan Leino

Reputation: 2087

The reason Dafny fails to verify the assertion assert stack.valid(); is the last conjunct in the body of valid():

(forall c :: c in contents ==>
  exists i,j :: 0 <= i < stack.Length 
             && 0 <= j < |stack[i]| 
             && stack[i][j] == c)

It has the form forall ... exists ..., and proving such a condition to be invariant is difficult for the verifier. Once you have figured out that this is the part of valid() that the verifier cannot prove (which you can do by, for example, manually inlining the definition of valid() in place of your assertion), then the solution is to give the verifier some assistance.

When the verifier--or a human, for that matter--tries to prove something for the form forall c :: P(c), then it makes up an arbitrary c and then tries to prove the "P(c)" for it. (Logicians call this rule "universal introduction".) Easy. Then, to prove something of the form exists i,j :: Q(i,j), the verifier looks for a witness to the "Q(i,j)". (This is known as "existential introduction".) Here, the verifier is not particularly creative and often needs help. Sometimes, you have to figure out some i and j yourself and then assert Q(i,j). Other times, it suffices to just mention some component of the needed Q(i,j) and the verifier will then figure out the rest. Exactly what to do can be a trial-and-error process.

What makes James's remedy above work is the fact that it mentions stack.stack[..] after the update truthAssignment[variable] := 1;. This tickles the verifier in a way that lets it see the light. Just writing the trivially proved assertion:

assert 0 <= |stack.stack[..]|;  // mentioning stack.stack[..] helps the verifier in the next line

after the update also works in this case.

Rustan

Upvotes: 2

James Wilcox
James Wilcox

Reputation: 5663

The following verifies for me:

assert stack.valid();
ghost var old_stack := stack.stack[..];
truthAssignment[variable] := 1;
assert stack.stack[..] == old_stack;
assert stack.valid();

I don't really understand why this works, but it falls under the general category of "extentional equality for sequences is hard for Dafny".

Upvotes: 1

Related Questions