1
Vote

Verification result depends on declaration order

description

The following two files (uploaded to rise4fun) are identical except for the order in which a lemma appears while the verification result is not the same.

An assertion error is produced when the lemma is the last declaration in the file; when it is the first, the file verifies correctly.

Tested at the command line with Dafny 1.9.7 and in rise4fun.

comments

rustanleino wrote Jul 2, 2016 at 2:06 AM

Thanks for the bug report (from April). There are two things going on with this example.

One thing is that there was a bug in Dafny in the checking of reads clause for multi-dimensional arrays. That has now been fixed (see https://dafny.codeplex.com/workitem/146). With this bug fix, Dafny complains about missing reads clauses. After adding the missing reads clauses, the programs both verify.

The other thing is that one gets different results depending on the declaration order (as the title of your report says). Sadly, this is still the case for your programs (without reads clauses) even after the bug fix of #146. (In the absence of the reads clauses--which Dafny now properly complains about--the frame axioms that Dafny uses allow you to derive false. My hunch is that the verifier doesn't always discover the proof of false in the same way, thus giving rise to different error reporting.) We are investing effort into eliminating or reducing these sorts of unpredictable results, so we appreciate your report.

Thanks,
Rustan

ruvus wrote Jul 4, 2016 at 11:23 AM

Thanks for your answer.

Using the current repository version from command line, the verifier produces different verification outcome not only without read clauses but also with them (reads edges in ValidGraph and PathCost).

When the lemma is the first declaration in the file, no errors are produced. When it is the last, an assertion violation is reported around line 126 with path[1..][..i] == path[1..i+1].