在Dafny中声明并初始化类对象数组的问题求助

问题代码 #

include "User.dfy"

class EnrollmentStation {
    var x : array<User>;
    constructor() {
        x := new User[2];
    }
}

报错信息 #

Undeclared top-level type or type parameter: User (did you forget to qualify a name or declare a module import 'opened'?)

解决建议 #

• 处理模块导入与访问权限
  如果User类定义在User.dfy的某个模块中，需要通过模块名限定类型，或者使用opened关键字导入模块以直接使用类型：

  // 方式1：用opened导入整个文件的内容
  opened include "User.dfy";
  
  class EnrollmentStation {
      var x : array<User>;
      constructor() {
          x := new User[2];
      }
  }
  

  或者如果User在指定模块内：

  include "User.dfy"
  
  class EnrollmentStation {
      // 用模块名限定User类型
      var x : array<UserModule.User>;
      constructor() {
          x := new UserModule.User[2];
      }
  }
  

• 确认文件路径正确性
  确保User.dfy与当前代码文件处于同一目录，若不在同一目录，需使用正确的相对路径引入，例如：

  include "../models/User.dfy"
  

• 检查User类的定义层级
  确保User类是User.dfy中的顶级类，而非嵌套在其他类或模块内部。如果是嵌套定义，需要调整其访问修饰符或修改引用方式。

补充：类对象数组的正确初始化示例 #

若User类包含带参数的构造函数，需要在数组初始化时显式调用构造函数：

class User {
    var name: string;
    constructor(n: string) {
        name := n;
    }
}

class EnrollmentStation {
    var x : array<User>;
    constructor() {
        // 初始化数组时为每个元素调用带参构造函数
        x := new User[2](i => new User($"User{i}"));
    }
}

内容的提问来源于stack exchange，提问作者Devin Bowman