A project I'm working on has a peculiar construct. I created a module like so:
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
}
}
I created another module with a different class like so:
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;
}
}
}
I'm not sure how to import/export modules in this construct. I tried redefining Module1
as abstract, but that does not work. If this is a wrong approach, a correct approach will be highly appreciated.
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;
}
}
}