renamed "abstract module" to "module facade"

renamed "ghost module" to "abstract module", adding a keyword "abstract"

5 files changed, 11 insertions, 11 deletions

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index c9545c93..fd445bc0 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -58,7 +58,7 @@ module CoRecursion {
   }

 }

 

-ghost module S {

+abstract module S {

   class C {

     var f: int;

     method m()

@@ -91,7 +91,7 @@ method NotMain() {
 }

 

 

-ghost module S1 {

+abstract module S1 {

   import B as S default T;

   static method do()

 }

diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy
index dbf39106..e4bd4605 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy
+++ b/Test/dafny0/RefinementModificationChecking.dfy
@@ -1,5 +1,5 @@
 

-ghost module R1 {

+abstract module R1 {

   var f: int;

   method m(y: set<int>) returns (r: int)

     modifies this;

@@ -8,7 +8,7 @@ ghost module R1 {
   }

 }

 

-ghost module R2 refines R1 {

+abstract module R2 refines R1 {

   var g: nat;

   method m ...

   {

diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 094e7be7..63c55506 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -4,7 +4,7 @@
 // Version with proof divided into stages:  June 2012.

 // Copyright (c) 2008-2012 Microsoft.

 

-ghost module M0 {

+abstract module M0 {

   // In this module, we declare the Node class, the definition of Reachability, and the specification

   // and implementation of the Schorr-Waite algorithm.

 

@@ -140,7 +140,7 @@ ghost module M0 {
   }

 }

 

-ghost module M1 refines M0 {

+abstract module M1 refines M0 {

   // In this superposition, we start reasoning about the marks.  In particular, we prove that the method

   // marks all reachable nodes.

   method SchorrWaite...

@@ -176,7 +176,7 @@ ghost module M1 refines M0 {
   }

 }

 

-ghost module M2 refines M1 {

+abstract module M2 refines M1 {

   // In this superposition, we prove that only reachable nodes are marked.  Essentially, we want

   // to add a loop invariant that says t is reachable from root, because then the loop invariant

   // that marked nodes are reachable follows.  More precisely, we need to say that the node

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index d8938aa7..93bf1812 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,4 +1,4 @@
-ghost module A {

+abstract module A {

   import L = Library;

   class {:autocontracts} StoreAndRetrieve<Thing> {

     ghost var Contents: set<Thing>;

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 := {};