Exclude fields from reads/modifies clause

[seebees]

If I know all the fields involved I can explain to Dafny who reads, modifies, and depends on what. However in a trait, I can not know all the possible fields that may exist. As such, I can not express that I do not depend on a specific field.

Take the following example that does not verify:

  trait Foo {
    var Modifies: set<object>
    predicate ValidState()
      reads this, Modifies
      ensures ValidState() ==> this !in Modifies

    var Bar: int

    method Baz()
      returns (output: string)
      requires ValidState()
      modifies this`Bar, Modifies
      ensures ValidState()
    {
      output := Whoops();
      Bar := Bar + 1;
    }

    method Whoops()
      returns (output: string)
      modifies Modifies
      ensures unchanged(this`Bar)
  }

Baz can not verify ValidState(). This is because ValidState reads this. So, in some given implementation of ValidState it MAY depend on Bar. But this is not the intention. The goal is to make Baz the arbiter of Bar. This is clear by the ensures unchanged(this`Bar)

I would like something reads this`!Bar that would mean “whatever the rest of the reads clause says, I definitely do not depend on the Bar field of this”.

Similarly, I would expect that modifies this`!Bar would be sugar for ensures unchanged(this`Bar)

[kjx]

I like this. If you're going to do it, I'd also like an untouched(this`Bar) to parallel unchanged(this`Bar) in they same way reads parallels modifies