dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.9k stars 260 forks source link

Default export set in abstract modules does not exist in refined module #2356

Open seebees opened 2 years ago

seebees commented 2 years ago

The following works as expected

abstract module Foo {

  export ExportSetName provides Bar

  datatype NotExported = NotExported
  method Bar() returns (r: int)
}

module Baz refines Foo {

  method Bar() returns(r: int) {
    return 5;
  }

}

module Use {
  import Baz`ExportSetName

  method Really?() returns (r: int) {
    r := Baz.Bar();
  }
}

However, if I remove the export set name, I get the error Error: no default export set declared in module: Baz

abstract module Foo {

  export provides Bar

  datatype NotExported = NotExported
  method Bar() returns (r: int)
}

module Baz refines Foo {

  method Bar() returns(r: int) {
    return 5;
  }

}

module Use {
  import Baz`ExportSetName

  method Really?() returns (r: int) {
    r := Baz.Bar();
  }
}

Tested in both Dafny 3.5 and 3.7

cpitclaudel commented 2 years ago

Good catch! I'm not sure why the default export set would be treated differently from named ones. If @RustanLeino confirms that this is indeed a bug the fix should be relatively easy.