Skip to content

Commit

Permalink
documentation: Fix missing abstract declarations (#874)
Browse files Browse the repository at this point in the history
The tutorial previously gave an example that was missing the `abstract` keyword in some module declarations.
  • Loading branch information
RustanLeino authored Sep 25, 2020
1 parent f21dd74 commit 2236b1f
Showing 1 changed file with 4 additions and 11 deletions.
15 changes: 4 additions & 11 deletions docs/OnlineTutorial/Modules.md
Original file line number Diff line number Diff line change
Expand Up @@ -453,11 +453,11 @@ In that case, you can use an *abstract* module import. In Dafny, this is written
is defined, any refinement of `B` can be used safely. For example, if we start with:

``` {.edit}
module Interface {
abstract module Interface {
function method addSome(n: nat): nat
ensures addSome(n) > n
}
module Mod {
abstract module Mod {
import A : Interface
method m() {
assert 6 <= A.addSome(5);
Expand All @@ -481,11 +481,11 @@ module Implementation refines Interface {
We can then substitute `Implementation` for `A` in a new module, by declaring a refinement of `Mod` which defines `A` to be `Implementation`.

``` {.editonly}
module Interface {
abstract module Interface {
function method addSome(n: nat): nat
ensures addSome(n) > n
}
module Mod {
abstract module Mod {
import A : Interface
method m() {
assert 6 <= A.addSome(5);
Expand All @@ -508,13 +508,6 @@ module Mod2 refines Mod {
}
```

```
module Mod2 refines Mod {
import A = Implementation
...
}
```

When you refine an abstract import into a concrete one, the concrete module must be an explicit refinement of the abstract one (i.e. declared with `refines`).


Expand Down

0 comments on commit 2236b1f

Please sign in to comment.