Made invariant of class 'ListOfMiningStrategies' robust by changing the design

(replaced public field by private field + getter/setter)

1 files changed, 19 insertions, 4 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 88a204a4..11c3670e 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2866,16 +2866,31 @@ namespace Microsoft.Boogie {
   }

 

   public class ListOfMiningStrategies : MiningStrategy {

-    public List<MiningStrategy>/*!*/ msList;

+

+    private List<MiningStrategy>/*!*/ _msList;

+

+    public List<MiningStrategy>/*!*/ msList

+    {

+      get

+      {

+        Contract.Ensures(Contract.Result<List<MiningStrategy>>() != null);

+        return this._msList;

+      }

+      set

+      {

+        Contract.Requires(value != null);

+        this._msList = value;

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(msList != null);

+      Contract.Invariant(this._msList != null);

     }

 

-

     public ListOfMiningStrategies(List<MiningStrategy> l) {

       Contract.Requires(l != null);

-      this.msList = l;

+      this._msList = l;

     }

   }