From 1188039043117d026e6cdfe13d35aed03880fea7 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Thu, 26 Aug 2010 23:38:33 +0000 Subject: Boogie: AIFramework port part 1/3: Committing new sources. --- Source/AIFramework/Functional.cs | 179 +++++++++++++++++++++++++++++++-------- 1 file changed, 144 insertions(+), 35 deletions(-) (limited to 'Source/AIFramework/Functional.cs') 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 /// Represents a functional collection of key/value pairs. /// 2 + [ContractClass(typeof(IFunctionalMapContracts))] public interface IFunctionalMap : System.Collections.ICollection, System.Collections.IEnumerable { /// Adds an element with the provided key and value to the . /// The to use as the value of the element to add. /// The to use as the key of the element to add. /// 2 - IFunctionalMap! Add(object! key, object value); + IFunctionalMap/*!*/ Add(object/*!*/ key, object value); /// /// Set the value of the key (that is already in the map) /// - IFunctionalMap! Set(object! key, object value); + IFunctionalMap/*!*/ Set(object/*!*/ key, object value); /// Determines whether the contains an element with the specified key. /// true if the contains an element with the key; otherwise, false. /// The key to locate in the . /// 2 [Pure] - bool Contains(object! key); + bool Contains(object/*!*/ key); /// Returns an for the . /// An for the . @@ -45,15 +46,107 @@ namespace Microsoft.AbstractInterpretationFramework.Collections /// Removes the element with the specified key from the . /// The key of the element to remove. /// 2 - IFunctionalMap! Remove(object! key); + IFunctionalMap/*!*/ Remove(object/*!*/ key); /// Gets an containing the values in the . /// An containing the values in the . /// 2 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() != null); + + throw new System.NotImplementedException(); +} + +IFunctionalMap IFunctionalMap.Set(object key, object value) +{ + Contract.Requires(key != null); + Contract.Ensures(Contract.Result() != 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() != null); + + throw new System.NotImplementedException(); +} + +ICollection IFunctionalMap.Values +{ + get { throw new System.NotImplementedException(); } +} + +object IFunctionalMap.this[object key] +{ + get {Contract.Ensures(Contract.Result() != 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 /// class FunctionalHashtable : IFunctionalMap { - private readonly Hashtable! h; + private readonly Hashtable/*!*/ h; + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(h != null); +} + /// /// Cannot directly construct an instance of a FunctionalHashtbl. @@ -78,43 +177,48 @@ namespace Microsoft.AbstractInterpretationFramework.Collections /// /// Cannot directly construct an instance of a FunctionalHashtbl. /// - 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != null); return string.Format("({0},{1},{2})", first, second, third); } } -- cgit v1.2.3