No verification error when "reads this" is missing

[benreynwar]

Dafny version

4.0.0.50303

Code to produce this issue

class MinimalError {
  var a: nat

  predicate valid()
    //reads this
    ensures valid() == (this.a == 0)

  method Blah()
    modifies this
    requires valid()
  {
    this.a := 2;
    assert false;
  }
}

Command to run and resulting output

Opened file in vscode.
It passes verification despite "assert false".
If the "reads this" in the predicate is uncommented it fails verification as expected.

What happened?

This example should fail verification.

What type of operating system are you experiencing the problem on?

Windows

[MikaelMayer]

That's strange, we are not raising the error that the predicate is reading "this" which is not part of its reads clause. That should be investigated. Anyway, even if this is possible in a postcondition now, it's not possible in a body.
What should happen here is that you should be warned that the predicate valid() which has a postcondition but no body.
Your predicates says it will not change value even if the object is modifies (since it does not read this).
This is like a lemma that says "I can prove a == 0 without reading the object", which leads to a contradiction once a has been assigned 2 that enables Dafny to prove false.

An upcoming PR will trigger a verification warning in your case
#3553
A verification warning will happen when you are assuming something which is not backed. Dafny will not let you compile this code, but I agree you should be notified.

[benreynwar]

That makes sense. Thanks for the explanation. Looking at #3553, it seems like this would give a warning for the current example but wouldn't help if valid was a ghost predicate. And the lack of a reads this feels like it should be an error rather than just a warning.

[benreynwar]

More generally, it would be nice to get a warning when I get into a state where a contradiction has been introduced. I'm new to dafny and my current approach is just to write assert false every now and then to double check I haven't made this mistake.

[rdivyanshu]

More generally, it would be nice to get a warning when I get into a state where a contradiction has been introduced. I'm new to dafny and my current approach is just to write assert false every now and then to double check I haven't made this mistake.

There are cases where you want to assert false. For example you are doing prove by case analysis and you want to convince Dafny that this case is impossible

[RustanLeino]

Postconditions of functions are not subject to reads checks. This is why the given postcondition is admitted. However, as @MikaelMayer pointed out, you won't be able to implement the body of valid(). This is similar to if you had written the untenable postcondition ensures false.

Presently, the warning that reminds you that valid() has no body is generated only if you compile your program. In the near future, that warning will appear earlier.

The best way to make sure your postcondition specifications are feasible is to provide an implementation. If for some reason you don't want to do that (for example, if the function or method is an extern, provided by some non-Dafny code), then you can use module refinement to supply a throwaway body (see https://github.com/dafny-lang/dafny/wiki/Modeling-External-State-Correctly). Similarly, the best way to make sure your precondition specifications are feasible is to provide a caller.

[RustanLeino]

I didn't check just now, but does the reference manual say that postconditions are not subject to reads checks? If so, then we can close this Issue. If not, then we should mark this issue with a Documentation tag.

[RustanLeino]

One more point on this subject, Dafny has an Auditor capability. It report things that a program accidentally or on purpose hides from the verifier. From the command line, you invoke it like

dafny audit test.dfy

[atomb]

In addition to the auditor, we're also in the design phase for an analysis that should be able to detect many cases of contradictory assumptions.

[benreynwar]

Great, thanks for all of this really useful information. I think the main point I was missing is that even for a ghost function I should be writing a body to help catch the bugs in my postconditions.

[benreynwar]

I tried to summarize the points made in an answer to my own question on stackoverflow.
https://stackoverflow.com/questions/76116578/assert-false-passing-verification-in-a-simple-class