Boogie: AIFramework port part 1/3: Committing new sources.

1 files changed, 144 insertions, 35 deletions

diff --git a/Source/AIFramework/Functional.cs b/Source/AIFramework/Functional.cs
index bee40031..e61adcc1 100644
--- a/Source/AIFramework/Functional.cs
+++ b/Source/AIFramework/Functional.cs
@@ -3,7 +3,7 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 

 namespace Microsoft.AbstractInterpretationFramework.Collections

 {

@@ -11,25 +11,26 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
 

     /// <summary>Represents a functional collection of key/value pairs.</summary>

     /// <filterpriority>2</filterpriority>

+    [ContractClass(typeof(IFunctionalMapContracts))]

     public interface IFunctionalMap : System.Collections.ICollection, System.Collections.IEnumerable

     {

         /// <summary>Adds an element with the provided key and value to the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>

         /// <param name="value">The <see cref="T:System.Object" /> to use as the value of the element to add. </param>

         /// <param name="key">The <see cref="T:System.Object" /> to use as the key of the element to add. </param>

         /// <filterpriority>2</filterpriority>

-        IFunctionalMap! Add(object! key, object value);

+        IFunctionalMap/*!*/ Add(object/*!*/ key, object value);

 

         /// <summary>

         /// Set the value of the key (that is already in the map)

         /// </summary>

-        IFunctionalMap! Set(object! key, object value);

+        IFunctionalMap/*!*/ Set(object/*!*/ key, object value);

         

         /// <summary>Determines whether the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" /> contains an element with the specified key.</summary>

         /// <returns>true if the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" /> contains an element with the key; otherwise, false.</returns>

         /// <param name="key">The key to locate in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />. </param>

         /// <filterpriority>2</filterpriority>

         [Pure]

-        bool Contains(object! key);

+        bool Contains(object/*!*/ key);

 

         /// <summary>Returns an <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>

         /// <returns>An <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</returns>

@@ -45,15 +46,107 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
         /// <summary>Removes the element with the specified key from the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>

         /// <param name="key">The key of the element to remove. </param>

         /// <filterpriority>2</filterpriority>

-        IFunctionalMap! Remove(object! key);

+        IFunctionalMap/*!*/ Remove(object/*!*/ key);

 

         /// <summary>Gets an <see cref="T:System.Collections.ICollection" /> containing the values in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>

         /// <returns>An <see cref="T:System.Collections.ICollection" /> containing the values in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</returns>

         /// <filterpriority>2</filterpriority>

         System.Collections.ICollection Values { get; }

  

-        object this [object! key] { get; /*set;*/ }

+        object this [object/*!*/ key] { get; /*set;*/ }

     }

+  [ContractClassFor(typeof(IFunctionalMap))]

+  public abstract class IFunctionalMapContracts:IFunctionalMap{

+

+  #region IFunctionalMap Members

+

+IFunctionalMap  IFunctionalMap.Add(object key, object value)

+{

+  Contract.Requires(key != null);

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

+

+ 	throw new System.NotImplementedException();

+}

+

+IFunctionalMap  IFunctionalMap.Set(object key, object value)

+{

+  Contract.Requires(key != null);

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

+

+ 	throw new System.NotImplementedException();

+}

+

+bool  IFunctionalMap.Contains(object key)

+{

+  Contract.Requires(key != null);

+

+ 	throw new System.NotImplementedException();

+}

+

+IDictionaryEnumerator  IFunctionalMap.GetEnumerator()

+{

+ 	throw new System.NotImplementedException();

+}

+

+ICollection  IFunctionalMap.Keys

+{

+	get { throw new System.NotImplementedException(); }

+}

+

+IFunctionalMap  IFunctionalMap.Remove(object key)

+{

+  Contract.Requires(key != null);

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

+

+ 	throw new System.NotImplementedException();

+}

+

+ICollection  IFunctionalMap.Values

+{

+	get { throw new System.NotImplementedException(); }

+}

+

+object  IFunctionalMap.this[object key]

+{

+	get {Contract.Ensures(Contract.Result<object>() != null);

+ throw new System.NotImplementedException(); }

+}

+

+#endregion

+

+#region ICollection Members

+

+void  ICollection.CopyTo(System.Array array, int index)

+{

+ 	throw new System.NotImplementedException();

+}

+

+int  ICollection.Count

+{

+	get { throw new System.NotImplementedException(); }

+}

+

+bool  ICollection.IsSynchronized

+{

+	get { throw new System.NotImplementedException(); }

+}

+

+object  ICollection.SyncRoot

+{

+	get { throw new System.NotImplementedException(); }

+}

+

+#endregion

+

+#region IEnumerable Members

+

+IEnumerator  IEnumerable.GetEnumerator()

+{

+ 	throw new System.NotImplementedException();

+}

+

+#endregion

+}

 

 

 

@@ -64,7 +157,13 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
     /// </summary>

     class FunctionalHashtable : IFunctionalMap

     {

-        private readonly Hashtable! h;

+        private readonly Hashtable/*!*/ h;

+      [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(h != null);

+}

+

 

         /// <summary>

         ///  Cannot directly construct an instance of a FunctionalHashtbl.

@@ -78,43 +177,48 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
         /// <summary>

         ///  Cannot directly construct an instance of a FunctionalHashtbl.

         /// </summary>

-        private FunctionalHashtable(Hashtable! h)

-        {

+        private FunctionalHashtable(Hashtable/*!*/ h){

+Contract.Requires(h != null);

             this.h = h;

             //            base();

         }

 

-        private static readonly IFunctionalMap! empty = new FunctionalHashtable();

-        public static IFunctionalMap! Empty { get { return empty; } }

+        private static readonly IFunctionalMap/*!*/ empty = new FunctionalHashtable();

+        public static IFunctionalMap/*!*/ Empty { get {Contract.Ensures(Contract.Result<IFunctionalMap>() != null);

+ return empty; } }

 

-        public IFunctionalMap! Add(object! key, object value)

-        {

+        public IFunctionalMap/*!*/ Add(object/*!*/ key, object value){

+Contract.Requires(key != null);

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

             Hashtable r = h.Clone() as Hashtable;

-            assume r != null;

+            Contract.Assume(r != null);

             r.Add(key, value);

             return new FunctionalHashtable(r);

         }

 

-        public IFunctionalMap! Set(object! key, object value) 

-        {

+        public IFunctionalMap/*!*/ Set(object/*!*/ key, object value){

+Contract.Requires(key != null);

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

             Hashtable r = h.Clone() as Hashtable;

         

-            assume r != null;

-            assert this.Contains(key);    // The entry must be defined

+            Contract.Assume(r != null);

+            Contract.Assert( this.Contains(key));    // The entry must be defined

              

             r[key] = value;
             return new FunctionalHashtable(r);

         }

 

         [Pure]

-        public bool Contains(object! key)

-        {

+        public bool Contains(object/*!*/ key){

+Contract.Requires(key != null);

             return h.Contains(key);

         }

         

         [Pure] [GlobalAccess(false)] [Escapes(true,false)]

-        IEnumerator! IEnumerable.GetEnumerator()

+        IEnumerator/*!*/ IEnumerable.GetEnumerator()

         {

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

+

             return h.GetEnumerator();

         }

         

@@ -129,10 +233,11 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
             get { return h.Keys; }

         }

 

-        public IFunctionalMap! Remove(object! key)

-        {

+        public IFunctionalMap/*!*/ Remove(object/*!*/ key){

+Contract.Requires(key != null);

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

             Hashtable r = h.Clone() as Hashtable;

-            assume r != null;

+            Contract.Assume(r != null);

             r.Remove(key);

             return new FunctionalHashtable(r);

         }

@@ -143,9 +248,9 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
         }

 

         

-        public object this[object! key]

+        public object this[object/*!*/ key]

         {

-            get { return h[key]; }       

+            get {Contract.Requires(key != null); return h[key]; }

         }

         

         public int Count

@@ -157,14 +262,18 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
         {

             [Pure] get { return h.IsSynchronized; }

         }

-        

-        public object! SyncRoot

+

+        public object/*!*/ SyncRoot

         {

-            [Pure] get { return h.SyncRoot; }

+          [Pure]

+          get {

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

+            return h.SyncRoot;

+          }

         }

         

-        public void CopyTo(System.Array! a, int index)

-        {

+        public void CopyTo(System.Array/*!*/ a, int index){

+Contract.Requires(a != null);

             h.CopyTo(a, index);

         }

     }

@@ -236,8 +345,8 @@ namespace Microsoft.AbstractInterpretationFramework.Collections.Generic
             return h;

         }

         

-        public override string! ToString()

-        {

+        public override string/*!*/ ToString() {

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

             return string.Format("({0},{1})", first, second);

         }

     }

@@ -276,8 +385,8 @@ namespace Microsoft.AbstractInterpretationFramework.Collections.Generic
             return h;

         }

         

-        public override string! ToString()

-        {

+        public override string/*!*/ ToString() {

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

             return string.Format("({0},{1},{2})", first, second, third);

         }

     }