diff options
| author |  tabarbe <unknown> | 2010-08-27 15:45:36 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-27 15:45:36 +0000 |
| commit | df0ba0f835f967289cb2a883e6322aed21cb9886 (patch) | |
| tree | b9ca307708849f15bf2aac38d7767a5c2006713f /Source/Basetypes/Set.cs | |
| parent | 506ce6e08d95c8664857dcb285b8c3f58f5c0bef (diff) | |
Boogie: Basetypes port 1/3: Committing new sources
Diffstat (limited to 'Source/Basetypes/Set.cs')
| -rw-r--r-- | Source/Basetypes/Set.cs | 476 |
1 files changed, 233 insertions, 243 deletions
diff --git a/Source/Basetypes/Set.cs b/Source/Basetypes/Set.cs index 9286d6f5..e31e5399 100644 --- a/Source/Basetypes/Set.cs +++ b/Source/Basetypes/Set.cs @@ -3,280 +3,270 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-namespace Microsoft.Boogie
-{
- using System;
- using System.IO;
- using System.Collections;
- using Microsoft.Contracts;
+namespace Microsoft.Boogie {
+ using System;
+ using System.IO;
+ using System.Collections;
+ using System.Diagnostics.Contracts;
+
+ /// <summary>
+ /// A class representing a mathematical set.
+ /// </summary>
+ public class Set : ICloneable, IEnumerable {
+ /*[Own]*/
+ Hashtable ht;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(ht != null);
+ }
+
+
+ public Set() {
+ ht = new Hashtable();
+ //:base();
+ }
+
+ private Set(Hashtable/*!*/ ht) {
+ Contract.Requires(ht != null);
+ this.ht = ht;
+ //:base();
+ }
+
+ public Set(int capacity) {
+ ht = new Hashtable(capacity);
+ //:base();
+ }
+
+
+ public readonly static Set/*!*/ Empty = new Set();
+
+ public void Clear() {
+ ht.Clear();
+ }
/// <summary>
- /// A class representing a mathematical set.
+ /// This method idempotently adds "o" to the set.
+ /// In notation:
+ /// this.SetElements = this.SetElements_old \union {o};
/// </summary>
- public class Set : ICloneable, IEnumerable
- {
- /*[Own]*/ Hashtable! ht;
-
- public Set()
- {
- ht = new Hashtable();
- base();
- }
+ public void Add(object/*!*/ o) {
+ Contract.Requires(o != null);
+ ht[o] = o;
+ }
- private Set(Hashtable! ht)
- {
- this.ht = ht;
- base();
- }
+ /// <summary>
+ /// this.SetElements = this.SetElements_old \union s.SetElements;
+ /// </summary>
+ public void AddRange(Set/*!*/ s) {
+ Contract.Requires(s != null);
+ foreach (object/*!*/ o in s) {
+ Contract.Assert(o != null);
+ Add(o);
+ }
+ }
- public Set(int capacity)
- {
- ht = new Hashtable(capacity);
- base();
- }
-
-
- public readonly static Set! Empty = new Set();
+ /// <summary>
+ /// this.SetElements = this.SetElements_old \setminus {o};
+ /// </summary>
+ public void Remove(object/*!*/ o) {
+ Contract.Requires(o != null);
+ ht.Remove(o);
+ }
- public void Clear()
- {
- ht.Clear();
+ /// <summary>
+ /// this.SetElements = this.SetElements_old \setminus s.SetElements;
+ /// </summary>
+ public void RemoveRange(Set/*!*/ s) {
+ Contract.Requires(s != null);
+ if (s == this) {
+ ht.Clear();
+ } else {
+ foreach (object/*!*/ o in s) {
+ Contract.Assert(o != null);
+ ht.Remove(o);
}
+ }
+ }
- /// <summary>
- /// This method idempotently adds "o" to the set.
- /// In notation:
- /// this.SetElements = this.SetElements_old \union {o};
- /// </summary>
- public void Add(object! o)
- {
- ht[o] = o;
- }
+ /// <summary>
+ /// Returns an arbitrary element from the set.
+ /// </summary>
+ public object/*!*/ Choose() {
+ Contract.Requires((Count > 0));
+ Contract.Ensures(Contract.Result<object>() != null);
+ IEnumerator iter = GetEnumerator();
+ iter.MoveNext();
+ return cce.NonNull(iter.Current);
+ }
- /// <summary>
- /// this.SetElements = this.SetElements_old \union s.SetElements;
- /// </summary>
- public void AddRange(Set! s)
- {
- foreach (object! o in s)
- {
- Add(o);
- }
- }
+ /// <summary>
+ /// Picks an arbitrary element from the set, removes it, and returns it.
+ /// </summary>
+ public object/*!*/ Take() {
+ Contract.Requires((Count > 0));
+ Contract.Ensures(Contract.Result<object>() != null);
+ Contract.Ensures(Count == Contract.OldValue(Count) - 1);
+ object r = Choose();
+ Remove(r);
+ return r;
+ }
- /// <summary>
- /// this.SetElements = this.SetElements_old \setminus {o};
- /// </summary>
- public void Remove(object! o)
- {
- ht.Remove(o);
+ public void Intersect(Set/*!*/ s) {
+ Contract.Requires(s != null);
+ Hashtable h = new Hashtable(ht.Count);
+ foreach (object/*!*/ key in ht.Keys) {
+ Contract.Assert(key != null);
+ if (s.ht.ContainsKey(key)) {
+ h.Add(key, key);
}
+ }
+ ht = h;
+ }
- /// <summary>
- /// this.SetElements = this.SetElements_old \setminus s.SetElements;
- /// </summary>
- public void RemoveRange(Set! s)
- {
- if (s == this)
- {
- ht.Clear();
- }
- else
- {
- foreach (object! o in s)
- {
- ht.Remove(o);
- }
- }
- }
-
- /// <summary>
- /// Returns an arbitrary element from the set.
- /// </summary>
- public object! Choose()
- requires Count > 0;
- {
- IEnumerator iter = GetEnumerator();
- iter.MoveNext();
- return (!)iter.Current;
- }
-
- /// <summary>
- /// Picks an arbitrary element from the set, removes it, and returns it.
- /// </summary>
- public object! Take()
- requires Count > 0;
- ensures Count == old(Count) - 1;
- {
- object r = Choose();
- Remove(r);
- return r;
+ /// <summary>
+ /// The getter returns true iff "o" is in the set.
+ /// The setter adds the value "o" (for "true") or removes "o" (for "false")
+ /// </summary>
+ public bool this[object/*!*/ o] {
+ get {
+ Contract.Requires(o != null);
+ return ht.ContainsKey(o);
+ }
+ set {
+ if (value) {
+ Add(o);
+ } else {
+ Remove(o);
}
+ }
+ }
- public void Intersect(Set! s)
- {
- Hashtable h = new Hashtable(ht.Count);
- foreach (object! key in ht.Keys)
- {
- if (s.ht.ContainsKey(key))
- {
- h.Add(key, key);
- }
- }
- ht = h;
- }
-
- /// <summary>
- /// The getter returns true iff "o" is in the set.
- /// The setter adds the value "o" (for "true") or removes "o" (for "false")
- /// </summary>
- public bool this[object! o]
- {
- get
- {
- return ht.ContainsKey(o);
- }
- set
- {
- if (value) {
- Add(o);
- } else {
- Remove(o);
- }
- }
- }
+ /// <summary>
+ /// Returns true iff "o" is an element of "this".
+ /// </summary>
+ /// <param name="o"></param>
+ /// <returns></returns>
+ [Pure]
+ public bool Contains(object/*!*/ o) {
+ Contract.Requires(o != null);
+ if (!this.ht.ContainsKey(o)) {
+ return false;
+ }
+ return true;
+ }
- /// <summary>
- /// Returns true iff "o" is an element of "this".
- /// </summary>
- /// <param name="o"></param>
- /// <returns></returns>
- [Pure]
- public bool Contains(object! o)
- {
- if (!this.ht.ContainsKey(o))
- {
+ /// <summary>
+ /// Returns true iff every element of "s" is an element of "this", that is, if
+ /// "s" is a subset of "this".
+ /// </summary>
+ /// <param name="s"></param>
+ /// <returns></returns>
+ public bool ContainsRange(Set/*!*/ s) {
+ Contract.Requires(s != null);
+ if (s != this) {
+ foreach (object/*!*/ key in s.ht.Keys) {
+ Contract.Assert(key != null);
+ if (!this.ht.ContainsKey(key)) {
return false;
- }
- return true;
+ }
}
+ }
+ return true;
+ }
- /// <summary>
- /// Returns true iff every element of "s" is an element of "this", that is, if
- /// "s" is a subset of "this".
- /// </summary>
- /// <param name="s"></param>
- /// <returns></returns>
- public bool ContainsRange(Set! s)
- {
- if (s != this)
- {
- foreach (object! key in s.ht.Keys)
- {
- if (!this.ht.ContainsKey(key))
- {
- return false;
- }
- }
- }
- return true;
- }
+ public object/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<object>() != null);
+ return new Set((Hashtable/*!*/)cce.NonNull(ht.Clone()));
+ }
- public object! Clone()
- {
- return new Set((Hashtable!)ht.Clone());
- }
+ public virtual int Count {
+ get {
+ return ht.Count;
+ }
+ }
- public virtual int Count
- {
- get
- {
- return ht.Count;
- }
- }
+ [Pure]
+ public IEnumerator/*!*/ GetEnumerator() {
+ Contract.Ensures(Contract.Result<IEnumerator>() != null);
+ return ht.Keys.GetEnumerator();
+ }
- [Pure]
- public IEnumerator! GetEnumerator()
- {
- return ht.Keys.GetEnumerator();
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ string s = null;
+ foreach (object/*!*/ key in ht.Keys) {
+ Contract.Assert(key != null);
+ if (s == null) {
+ s = "{";
+ } else {
+ s += ", ";
}
+ s += key.ToString();
+ }
+ if (s == null) {
+ return "{}";
+ } else {
+ return s + "}";
+ }
+ }
- [Pure]
- public override string! ToString()
- {
- string s = null;
- foreach (object! key in ht.Keys)
- {
- if (s == null)
- {
- s = "{";
- }
- else
- {
- s += ", ";
- }
- s += key.ToString();
- }
- if (s == null)
- {
- return "{}";
- }
- else
- {
- return s + "}";
- }
- }
-
- public bool AddAll(IEnumerable! objs){
- foreach (object! o in objs){
- this.Add(o);
- }
- return true;
- }
- //----------------------------- Static Methods ---------------------------------
-
- // Functional Intersect
- public static Set! Intersect(Set! a, Set! b)
- // ensures Forall{ object x in result; a[x] && b[x] };
- {
- Set! res = (Set!) a.Clone();
- res.Intersect(b);
- return res;
- }
- // Functional Union
- public static Set! Union(Set! a, Set! b)
- // ensures Forall{ object x in result; a[x] || b[x] };
- {
- Set! res = (Set!) a.Clone();
- res.AddRange(b);
- return res;
- }
-
- public delegate bool SetFilter(object! obj);
+ public bool AddAll(IEnumerable/*!*/ objs) {
+ Contract.Requires(objs != null);
+ foreach (object/*!*/ o in objs) {
+ Contract.Assert(o != null);
+ this.Add(o);
+ }
+ return true;
+ }
+ //----------------------------- Static Methods ---------------------------------
+
+ // Functional Intersect
+ public static Set/*!*/ Intersect(Set/*!*/ a, Set/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<Set>() != null);
+ //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
+ Set/*!*/ res = (Set/*!*/)cce.NonNull(a.Clone());
+ res.Intersect(b);
+ return res;
+ }
+ // Functional Union
+ public static Set/*!*/ Union(Set/*!*/ a, Set/*!*/ b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ Contract.Ensures(Contract.Result<Set>() != null);
+ // Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
+ Set/*!*/ res = (Set/*!*/)cce.NonNull(a.Clone());
+ res.AddRange(b);
+ return res;
+ }
+
+ public delegate bool SetFilter(object/*!*/ obj);
- public static Set! Filter(Set! a, SetFilter! filter)
- {
- Set inter = new Set();
+ public static Set/*!*/ Filter(Set/*!*/ a, SetFilter/*!*/ filter) {
+ Contract.Requires(filter != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<Set>() != null);
+ Set inter = new Set();
- foreach(object! elem in a)
- {
- if (filter(elem))
- {
- inter.Add(elem);
- }
- }
- return inter;
- }
+ foreach (object/*!*/ elem in a) {
+ Contract.Assert(elem != null);
+ if (filter(elem)) {
+ inter.Add(elem);
+ }
+ }
+ return inter;
+ }
}
-
- public interface IWorkList: ICollection
- {
+
+ public interface IWorkList : ICollection {
bool Add(object o);
bool AddAll(IEnumerable objs);
bool IsEmpty();
object Pull();
}
-
+
}
\ No newline at end of file |