Search code examples
dafnyformal-verification

accessing members of constrained type parameters in Dafny

Dafny neophyte here (again!). Below, Scope is fine, but the 'generic' version ScopeG fails with type T does not have a member id on the line forall id :: id in id2Items ==> id == id2Items[id].id. I'd like to understand why that might be the case.

trait Identified {
  const id: string
}

trait Scope {
  const id2Items: map<string, Identified>

  predicate Valid()
    reads this
  {
    forall id :: id in id2Items ==> id == id2Items[id].id
  }
}

trait ScopeG<T extends Identified> {
  const id2Items: map<string, T>

  predicate Valid()
    reads this
  {
    forall id :: id in id2Items ==> id == id2Items[id].id
  }
}

I'm using Dafny 4.8.1.

Solution

  • To use a T as its bound Identified, you first have to cast it:

    forall id :: id in id2Items ==> id == (id2Items[id] as Identified).id

    This may change in the future to make the explicit cast unnecessary.