diff options
Diffstat (limited to 'Test/dafny3')
-rw-r--r-- | Test/dafny3/CachedContainer.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny3/CachedContainer.dfy b/Test/dafny3/CachedContainer.dfy index 9bde80da..6ac5ff2f 100644 --- a/Test/dafny3/CachedContainer.dfy +++ b/Test/dafny3/CachedContainer.dfy @@ -1,5 +1,5 @@ -// give the method signatures and specs
-ghost module M0 {
+// give the method signatures and specs
+abstract module M0 {
class {:autocontracts} Container<T(==)> {
ghost var Contents: set<T>;
predicate Valid()
@@ -16,7 +16,7 @@ ghost module M0 { }
// provide bodies for the methods
-ghost module M1 refines M0 {
+abstract module M1 refines M0 {
class Container<T(==)> {
constructor... {
Contents := {};
|