在另一个模块的类中创建类对象

Question

我正在从事的一个项目有一个特殊的结构。我创建了一个像这样的模块：

module Module1 {
    export Private
        provides test1
        reveals test1, T

    class test1{
        var a: nat
        var b: nat

        constructor()
        {
            a := 0;
            b := 0;
        }

        method add() returns (c: nat) 
            ensures c == a + b
        {
            c := a + b;
        }
    }

    trait T {
        var x: nat

        predicate valid()
            reads this
    }
}

我创建了另一个具有不同类的模块，如下所示：

include "module1.dfy"

module Module2 refines Module1 {
    import opened Module1`Private

    class test2{
        var d: nat
        var module1Obj: test1

        constructor() {
            d := 0;
            module1Obj := new Module1.test1(); // ERROR: type Module1.test1 is not assignable to LHS (of type test1)
        }
    }

    class test3 extends T {
        predicate valid() {
            x == 0
        }

        constructor()
            ensures valid()
        {
            x := 0;
        }
    }
}

我不确定如何在此构造中导入/导出模块。我尝试将

Module1

重新定义为抽象，但这不起作用。如果这是错误的方法，我们将高度赞赏正确的方法。

Answer 1

include "module1.dfy"

module Module2 refines Module1 {
    import opened Module1`Private

    class test2{
        var d: nat
        var module1Obj: Module1.test1

        constructor() {
            d := 0;
            module1Obj := new Module1.test1(); // ERROR: type Module1.test1 is not assignable to LHS (of type test1)
        }
    }

    class test3 extends T {
        predicate valid() 
            reads this
        {
            x == 0
        }

        constructor()
            ensures valid()
        {
            x := 0;
        }
    }
}