Dafny中约束类型参数的成员访问报错问题求助

你遇到的问题是Dafny泛型约束的语法使用错误导致的。

报错原因 #

Dafny中，针对trait的泛型参数约束，应该使用is关键字而非extends。extends主要用于类之间的继承关系声明，而trait作为接口性质的抽象类型，需要用is来指定泛型参数是该trait的实现类型。

你的代码中ScopeG<T extends Identified>使用了extends，导致Dafny无法正确识别T继承了Identified中的const id成员，因此在访问id2Items[id].id时会报错“type T does not have a member id”。

修复后的代码 #

将泛型约束的extends替换为is即可解决问题：

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 is Identified> {
  const id2Items: map<string, T>

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

补充说明 #

• 约束泛型参数实现某个trait时，统一使用T is TraitName的语法；
• extends仅用于类继承另一个类的场景，比如class MyClass extends BaseClass；
• 替换后，Dafny就能正确推断T包含Identified中的id成员，验证逻辑可以正常通过。

内容的提问来源于stack exchange，提问作者Sam Stainsby