diff options
Diffstat (limited to 'Source/Core/PureCollections.cs')
| -rw-r--r-- | Source/Core/PureCollections.cs | 990 |
1 files changed, 582 insertions, 408 deletions
diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs index e6d68a34..a77f59a1 100644 --- a/Source/Core/PureCollections.cs +++ b/Source/Core/PureCollections.cs @@ -13,140 +13,184 @@ using System;
using System.Collections;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
namespace PureCollections {
//-------------------------------------------------------------------
// General types
//-------------------------------------------------------------------
- public class MissingCase :Exception{}
+ public class MissingCase : Exception {
+ }
- public struct Capacity{
+ public struct Capacity {
public int capacity;
- public Capacity (int i) {capacity = i;}
+ public Capacity(int i) {
+ capacity = i;
+ }
}
abstract public class Coll {
public object[] elems; // null is used to show empty spots!
protected int card;
- protected Coll() {}
- protected Coll(object[] elems, int card) {this.elems = elems; this.card = card; }
- protected Coll(Coll! c)
- requires c.elems != null;
- {
- this.elems = (object[])c.elems.Clone();
- this.card = c.card;
- }
- }
+ protected Coll() {
+ }
+ protected Coll(object[] elems, int card) {
+ this.elems = elems;
+ this.card = card;
+ }
+ protected Coll(Coll c) {
+ Contract.Requires(c != null);
+ Contract.Requires(c.elems != null);
+ this.elems = (object[])c.elems.Clone();
+ this.card = c.card;
+ }
+ }
// ------------------------------------------------------------------
// Tuple
// ------------------------------------------------------------------
- public class Tuple : Coll, IComparable
- {
+ public class Tuple : Coll, IComparable {
//public object[] elems;
-
+
//invariant this.elems != null;
// Constructor - - - - - - - - - - - - - - - - - - - - - - - - - -
- public Tuple(params object []! ts) {
- elems = ts;
- card = ts.Length;}
+ public Tuple(params object[] ts) {
+ Contract.Requires(ts != null);
+ elems = ts;
+ card = ts.Length;
+ }
public Tuple(Capacity c) {
- elems = new object[c.capacity];
- card = c.capacity;
- }
+ elems = new object[c.capacity];
+ card = c.capacity;
+ }
//Equality - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals (object o){
- assert this.elems != null;
- if (o == null || !(o is Tuple) || elems.Length != ((!)((Tuple)o).elems).Length)
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object o) {
+ Contract.Assert(this.elems != null);
+ if (o == null || !(o is Tuple) || elems.Length != (cce.NonNull((Tuple)o).elems).Length)
return false;
- Tuple s = (Tuple) o; - for(int i = 0; i < elems.Length; i ++)
- if ( ! Equals(this.elems[i], s.elems[i]))
+ Tuple s = (Tuple)o;
+ for (int i = 0; i < elems.Length; i++)
+ if (!Equals(this.elems[i], s.elems[i]))
return false;
return true;
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
- public static bool operator == (Tuple s, Tuple t) {return s == null ? t == null : s.Equals(t);}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
- public static bool operator != (Tuple s, Tuple t) { return ! (t == s); }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
+ public static bool operator ==(Tuple s, Tuple t) {
+ return s == null ? t == null : s.Equals(t);
+ }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
+ public static bool operator !=(Tuple s, Tuple t) {
+ return !(t == s);
+ }
[Pure]
- public override int GetHashCode (){
- int h =0;
- assume this.elems != null;
- for(int i = 0; i < elems.Length; i++)
- {
+ public override int GetHashCode() {
+ int h = 0;
+ Contract.Assume(this.elems != null);
+ for (int i = 0; i < elems.Length; i++) {
object elem = elems[i];
- if (elem != null)
+ if (elem != null)
h += elem.GetHashCode();
}
- return h; + return h;
}
//Compare - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- int IComparable.CompareTo(object o) {
- assert this.elems != null;
- if (o == null || !(o is Tuple) || elems.Length != ((!)((Tuple)o).elems).Length)
+ int IComparable.CompareTo(object o) {
+ Contract.Assert(this.elems != null);
+ if (o == null || !(o is Tuple) || elems.Length != (cce.NonNull((Tuple)o).elems).Length)
throw new MissingCase();
-
- Tuple t = (Tuple) o;
- for(int i = 0; i < elems.Length; i ++) {
- int c = ((IComparable!) elems[i]).CompareTo(t.elems[i]);
- if (c < 0) return -1;
- else if (c > 0) return +1;
+
+ Tuple t = (Tuple)o;
+ for (int i = 0; i < elems.Length; i++) {
+ int c = cce.NonNull((IComparable)elems[i]).CompareTo(t.elems[i]);
+ if (c < 0)
+ return -1;
+ else if (c > 0)
+ return +1;
}
return 0;
}
- public static bool operator <= (Tuple s, Tuple t) {return s == null ? t == null : ((IComparable) s).CompareTo(t) <= 0;}
- public static bool operator < (Tuple s, Tuple t) {return s == null ? false : ((IComparable) s).CompareTo(t) < 0;}
- public static bool operator >= (Tuple s, Tuple t) {return t <= s; }
- public static bool operator > (Tuple s, Tuple t) { return t < s; }
+ public static bool operator <=(Tuple s, Tuple t) {
+ return s == null ? t == null : ((IComparable)s).CompareTo(t) <= 0;
+ }
+ public static bool operator <(Tuple s, Tuple t) {
+ return s == null ? false : ((IComparable)s).CompareTo(t) < 0;
+ }
+ public static bool operator >=(Tuple s, Tuple t) {
+ return t <= s;
+ }
+ public static bool operator >(Tuple s, Tuple t) {
+ return t < s;
+ }
//Select and Update - - - - - - - - - - - - - - - - - - - - - - - -
- public object this[int index]{
- get{assert this.elems != null; return elems[index];}
- set{assert this.elems != null; elems[index] = value;}
+ public object this[int index] {
+ get {
+ Contract.Assert(this.elems != null);
+ return elems[index];
+ }
+ set {
+ Contract.Assert(this.elems != null);
+ elems[index] = value;
+ }
}
-
+
//ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[Pure]
- public override string! ToString() {
- assert this.elems != null; - if (elems.Length==0)
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ Contract.Assert(this.elems != null);
+ if (elems.Length == 0)
return "()";
-
+
string s = "(";
- for (int i= 0; i< elems.Length-1; i++)
- s += ((!)elems[i]).ToString() + ", ";
- return s + ((!)elems[elems.Length-1]).ToString() + ")";
- }
+ for (int i = 0; i < elems.Length - 1; i++)
+ s += cce.NonNull(elems[i]).ToString() + ", ";
+ return s + cce.NonNull(elems[elems.Length - 1]).ToString() + ")";
+ }
}
// ------------------------------------------------------------------
// Pair
- public class Pair : Tuple{
- protected Pair(){}
+ public class Pair : Tuple {
+ protected Pair() {
+ }
public Pair(object first, object second) {
- elems = new object[]{first,second};
+ elems = new object[] { first, second };
}
- public object First{
- get{assert this.elems != null; return elems[0];}
- set{assert this.elems != null; elems[0]=value;}
+ public object First {
+ get {
+ Contract.Assert(this.elems != null);
+ return elems[0];
+ }
+ set {
+ Contract.Assert(this.elems != null);
+ elems[0] = value;
+ }
}
- public object Second{
- get{assert this.elems != null; return elems[1];}
- set{assert this.elems != null; elems[1]=value;}
+ public object Second {
+ get {
+ Contract.Assert(this.elems != null);
+ return elems[1];
+ }
+ set {
+ Contract.Assert(this.elems != null);
+ elems[1] = value;
+ }
}
}
@@ -154,106 +198,137 @@ namespace PureCollections { // Map
// --------------------------------------------------------------------
- public class MapEnumerator: IEnumerator{
- private Map! map;
+ public class MapEnumerator : IEnumerator {
+ private Map/*!*/ map;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(map != null);
+ }
+
private int index = -1;
- public MapEnumerator(Map! m) { map = m;}
+ public MapEnumerator(Map m) {
+ Contract.Requires(m != null);
+ map = m;
+ }
public bool MoveNext() {
- do{
+ do {
index++;
- assert map.elems != null;
+ Contract.Assert(map.elems != null);
} while (index < map.elems.Length && map.elems[index] == null);
return index < map.elems.Length;
}
- public object Current{ get { assert map.elems != null; return new Pair(map.elems[index],map.vals[index]); }}
- public void Reset() {index = -1; }
+ public object Current {
+ get {
+ Contract.Assert(map.elems != null);
+ return new Pair(map.elems[index], map.vals[index]);
+ }
+ }
+ public void Reset() {
+ index = -1;
+ }
}
-
- public class Map:Coll, IEnumerable, IComparable
- {
- public Object[]! vals;
-
+
+ public class Map : Coll, IEnumerable, IComparable {
+ public Object[]/*!*/ vals;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(vals != null);
+ }
+
+
//invariant this.elems != null;
-
+
// constructors - - - - - - - - - - - - - - - - - - - - - - - - - - -
- public Map(Capacity c){
- elems = new Object[c.capacity*2];
- vals = new Object[c.capacity*2];
+ public Map(Capacity c) {
+ elems = new Object[c.capacity * 2];
+ vals = new Object[c.capacity * 2];
card = 0;
}
-
+
[NotDelayed]
- public Map(params Pair []! ps){
- elems = new Object[ps.Length*2];
- vals = new Object[ps.Length*2];
- base();
+ public Map(params Pair[] ps)
+ : base() {//BASEMOVE DANGER
+ Contract.Requires(ps != null);
+ elems = new Object[ps.Length * 2];
+ vals = new Object[ps.Length * 2];
+ //base();
card = 0;
- for(int i = 0; i < ps.Length; i++)
- Insert( ((!)ps[i]).First, ((!)ps[i]).Second);
+ for (int i = 0; i < ps.Length; i++)
+ Insert(cce.NonNull(ps[i]).First, cce.NonNull(ps[i]).Second);
}
// iterators - - - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure] [GlobalAccess(false)] [Escapes(true,false)]
- public IEnumerator! GetEnumerator() {
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ public IEnumerator GetEnumerator() {
+ Contract.Ensures(Contract.Result<IEnumerator>() != null);
return new MapEnumerator(this);
}
public Pair[] ToArray() {
- Pair [] n = new Pair[card];
+ Pair[] n = new Pair[card];
int ct = 0;
- assert this.elems != null;
- for(int i =0; i < elems.Length ; i++)
+ Contract.Assert(this.elems != null);
+ for (int i = 0; i < elems.Length; i++)
if (elems[i] != null)
n[ct++] = new Pair(elems[i], vals[i]);
return n;
}
-
+
//(ASM) Update- - - - - - - - - - - - - - - - - - - - - - - - - - -
public Map Update(object k, object v) {
- Map n = new Map(new Capacity(card+1));
- assert this.elems != null;
- for (int i = 0; i < elems.Length; i++ )
- if (elems[i] != null && ! Equals(elems[i], k))
+ Map n = new Map(new Capacity(card + 1));
+ Contract.Assert(this.elems != null);
+ for (int i = 0; i < elems.Length; i++)
+ if (elems[i] != null && !Equals(elems[i], k))
n.Insert(elems[i], vals[i]);
- n.Insert(k,v);
+ n.Insert(k, v);
return n;
}
//In place Update (and Remove)- - - - - - - - - - - - - - - - - - -
- public object this[object index]{
- get{return this.Apply(index);}
- set{this.Insert(index,value);}
- }
-
- public void Remove(object! o) {
- assert this.elems != null;
- int h = Math.Abs(o.GetHashCode()) % elems.Length;
- for (int i = 0; i < elems.Length; i++ ) {
- int j = (i+ h) % elems.Length;
- if (elems[j] == null) {
- break;
- } else if (Equals(elems[j], o)){
- elems[j] = null;
- vals[j] = null;
- break;
- }
- }
+ public object this[object index] {
+ get {
+ return this.Apply(index);
+ }
+ set {
+ this.Insert(index, value);
+ }
+ }
+
+ public void Remove(object o) {
+ Contract.Requires(o != null);
+ Contract.Assert(this.elems != null);
+ int h = Math.Abs(o.GetHashCode()) % elems.Length;
+ for (int i = 0; i < elems.Length; i++) {
+ int j = (i + h) % elems.Length;
+ if (elems[j] == null) {
+ break;
+ } else if (Equals(elems[j], o)) {
+ elems[j] = null;
+ vals[j] = null;
+ break;
}
-
+ }
+ }
+
public void Insert(Object key, Object val) {
if (key == null)
- throw new MissingCase(); -
- assert this.elems != null;
- if (elems.Length == 0 || 2*card >= elems.Length){
- int m = card*2; if (m < 4) m = 4;
- object [] newElems = new object [m];
- object [] newVals = new object [m];
+ throw new MissingCase();
+
+ Contract.Assert(this.elems != null);
+ if (elems.Length == 0 || 2 * card >= elems.Length) {
+ int m = card * 2;
+ if (m < 4)
+ m = 4;
+ object[] newElems = new object[m];
+ object[] newVals = new object[m];
for (int k = 0; k < elems.Length; k++) {
object elem = elems[k];
if (elem != null) {
int newHash = Math.Abs(elem.GetHashCode()) % newElems.Length;
- for (int i = 0; i < newElems.Length; i++ ) {
- int j = (i+ newHash) % newElems.Length;
+ for (int i = 0; i < newElems.Length; i++) {
+ int j = (i + newHash) % newElems.Length;
if (newElems[j] == null) {
newElems[j] = elem;
newVals[j] = vals[k];
@@ -264,17 +339,17 @@ namespace PureCollections { }
elems = newElems;
vals = newVals;
- }
+ }
int h = Math.Abs(key.GetHashCode()) % elems.Length;
- for (int i = 0; i < elems.Length; i++ ) {
- int j = (i+ h) % elems.Length;
+ for (int i = 0; i < elems.Length; i++) {
+ int j = (i + h) % elems.Length;
if (elems[j] == null) {
elems[j] = key;
vals[j] = val;
- card ++;
+ card++;
return;
} else if (key.Equals(elems[j])) {
- vals[j] = val; + vals[j] = val;
return;
}
}
@@ -282,24 +357,26 @@ namespace PureCollections { //ToString - - - - - - - - - - - - - - - - - - - - - - - - -
[Pure]
- public override string! ToString() {
- if (card ==0)
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ if (card == 0)
return "{|->}";
else {
- string s = "{"; int ct = 0;
- assert this.elems != null;
- for(int i =0; i < elems.Length ; i++) {
+ string s = "{";
+ int ct = 0;
+ Contract.Assert(this.elems != null);
+ for (int i = 0; i < elems.Length; i++) {
object elem = elems[i];
- if (elem != null){
- s += elem.ToString() +"|->" + ((!)vals[i]).ToString() ;
- s +=(ct!=card-1) ? ", " : "";
- ct ++;
+ if (elem != null) {
+ s += elem.ToString() + "|->" + cce.NonNull(vals[i]).ToString();
+ s += (ct != card - 1) ? ", " : "";
+ ct++;
}
- }
- return s+"}";
+ }
+ return s + "}";
}
}
-
+
// Subset operations - - - - - - - - - - - - - - - - - - - - - - -
// View Map as Set of Pairs
@@ -307,175 +384,212 @@ namespace PureCollections { if (o == null || !(o is Map))
throw new MissingCase();
// WS Improve performance!
- Map t = (Map) o;
- if (this < t) return -1;
- else if(this > t) return +1;
- else return 0;
- }
- public static bool operator <= (Map s, Map t){
- if (s==null) return t==null;
- if (t==null) return false;
- assert s.elems != null;
- for(int i = 0; i < s.elems.Length; i++)
- if (s.elems[i]!= null) {
+ Map t = (Map)o;
+ if (this < t)
+ return -1;
+ else if (this > t)
+ return +1;
+ else
+ return 0;
+ }
+ public static bool operator <=(Map s, Map t) {
+ if (s == null)
+ return t == null;
+ if (t == null)
+ return false;
+ Contract.Assert(s.elems != null);
+ for (int i = 0; i < s.elems.Length; i++)
+ if (s.elems[i] != null) {
object o = t.Apply(s.elems[i]);
if (o == null || !o.Equals(s.vals[i]))
return false;
}
- return true; + return true;
}
- public static bool operator < (Map s, Map t){
- return s == null || t == null ? false : s.card < t.card && s <= t; + public static bool operator <(Map s, Map t) {
+ return s == null || t == null ? false : s.card < t.card && s <= t;
}
- public static bool operator >= (Map s, Map t){
- return t <= s; - }
- public static bool operator > (Map s, Map t){
- return t < s; + public static bool operator >=(Map s, Map t) {
+ return t <= s;
+ }
+ public static bool operator >(Map s, Map t) {
+ return t < s;
}
// Equality - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals (Object t){
- return t != null && t is Map && card == ((Map) t).card && this<= ((Map) t);
- }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
- public static bool operator == (Map s, Map t){
- if ((object)s==null)
- if ((object)t==null) return true;
- else return t.Equals(s);
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(Object t) {
+ return t != null && t is Map && card == ((Map)t).card && this <= ((Map)t);
+ }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
+ public static bool operator ==(Map s, Map t) {
+ if ((object)s == null)
+ if ((object)t == null)
+ return true;
+ else
+ return t.Equals(s);
else
return s.Equals(t);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
- public static bool operator != (Map s, Map t){
- return ! (t == s); + [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
+ public static bool operator !=(Map s, Map t) {
+ return !(t == s);
}
[Pure]
- public override int GetHashCode (){
- int h =0;
- assert this.elems != null;
- for(int i = 0; i < elems.Length; i++)
- {
+ public override int GetHashCode() {
+ int h = 0;
+ Contract.Assert(this.elems != null);
+ for (int i = 0; i < elems.Length; i++) {
object elem = elems[i];
- if (elem != null)
- {
- h += elem.GetHashCode() + ((!)vals[i]).GetHashCode();
+ if (elem != null) {
+ h += elem.GetHashCode() + cce.NonNull(vals[i]).GetHashCode();
}
}
- return h; + return h;
}
-
+
//Ordinary map operations- - - - - - - - - - - - - - - - - - - - - - - -
-
+
[Pure]
- public bool Has(Object x) {
- if (x == null)
- throw new MissingCase(); + public bool Has(Object x) {
+ if (x == null)
+ throw new MissingCase();
- assert this.elems != null;
- if (elems.Length == 0)
+ Contract.Assert(this.elems != null);
+ if (elems.Length == 0)
return false;
int h = Math.Abs(x.GetHashCode()) % elems.Length;
- for (int i = 0; i < elems.Length; i++ ) {
- int j = (i+ h) % elems.Length;
+ for (int i = 0; i < elems.Length; i++) {
+ int j = (i + h) % elems.Length;
if (x.Equals(elems[j]))
return true;
}
return false;
}
- public object Apply(object x) {
+ public object Apply(object x) {
if (x == null)
throw new MissingCase();
- assert this.elems != null;
- if (elems.Length == 0)
+ Contract.Assert(this.elems != null);
+ if (elems.Length == 0)
return null;
int h = Math.Abs(x.GetHashCode()) % elems.Length;
- for (int i = 0; i < elems.Length; i++ ) {
- int j = (i+ h) % elems.Length;
+ for (int i = 0; i < elems.Length; i++) {
+ int j = (i + h) % elems.Length;
if (elems[j] != null && x.Equals(elems[j]))
return vals[j];
}
- return null; + return null;
}
- public static Map Override(Map! s, Map! t) {
- Map m = new Map(new Capacity(s.card+t.card));
- assert s.elems != null;
- for(int i = 0; i< s.elems.Length; i++)
- if (s.elems[i] != null)
+ public static Map Override(Map s, Map t) {
+ Contract.Requires(t != null);
+ Contract.Requires(s != null);
+ Map m = new Map(new Capacity(s.card + t.card));
+ Contract.Assert(s.elems != null);
+ for (int i = 0; i < s.elems.Length; i++)
+ if (s.elems[i] != null)
m.Insert(s.elems[i], s.vals[i]);
- assert t.elems != null;
- for(int i = 0; i< t.elems.Length; i++)
- if (t.elems[i] != null)
+ Contract.Assert(t.elems != null);
+ for (int i = 0; i < t.elems.Length; i++)
+ if (t.elems[i] != null)
m.Insert(t.elems[i], t.vals[i]);
- return m; - }
+ return m;
+ }
}
// --------------------------------------------------------------------
// Sequence
- public class SequenceEnumerator: IEnumerator{
- [Peer] private Sequence! seq;
+ public class SequenceEnumerator : IEnumerator {
+ [Peer]
+ private Sequence/*!*/ seq;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(seq != null);
+ }
+
private int index = -1;
[Captured]
- public SequenceEnumerator(Sequence! s) { seq = s;}
+ public SequenceEnumerator(Sequence s) {
+ Contract.Requires(s != null);
+ seq = s;
+ }
public bool MoveNext() {
index++;
//while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null);
return index < seq.Length;
}
- public object Current{ get { assert seq.elems != null; return seq.elems[index]; }}
- public void Reset() {index = -1; }
+ public object Current {
+ get {
+ Contract.Assert(seq.elems != null);
+ return seq.elems[index];
+ }
+ }
+ public void Reset() {
+ index = -1;
+ }
}
-
- public class Sequence:Coll, IEnumerable, IComparable
- {
- public Sequence(){elems = new object [4];}
-
+
+ public class Sequence : Coll, IEnumerable, IComparable {
+ public Sequence() {
+ elems = new object[4];
+ }
+
//invariant this.elems != null;
//constructors - - - - - - - - - - - - - - - - - - - - - - - - - - -
- public Sequence(params object []! ds){card = ds.Length; elems = ds; }
- public Sequence(Sequence! seq) {
- base(seq);
+ public Sequence(params object[] ds) {
+ Contract.Requires(ds != null);
+ card = ds.Length;
+ elems = ds;
+ }
+ public Sequence(Sequence seq)
+ : base(seq) {//BASEMOVEA
+ Contract.Requires(seq != null);
+ //base(seq);
+ }
+ public Sequence(Capacity c) {
+ elems = new object[c.capacity];
}
- public Sequence(Capacity c){elems = new object [c.capacity];}
// Iterators - - - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure] [GlobalAccess(false)] [Escapes(true,false)]
- public IEnumerator! GetEnumerator()
- ensures Owner.Same(result, this);
- ensures result.IsNew;
- {
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ public IEnumerator/*!*/ GetEnumerator() {
+ Contract.Ensures(cce.Owner.Same(Contract.Result<IEnumerator>(), this));
+ Contract.Ensures(Contract.Result<IEnumerator>() != null);
+ Contract.Ensures(cce.IsNew(Contract.Result<IEnumerator>()));
return new SequenceEnumerator(this);
}
-
+
public object[] ToArray() {
- object [] n = new object[card];
+ object[] n = new object[card];
int ct = 0;
- assert this.elems != null;
- for(int i =0; i < elems.Length ; i++)
+ Contract.Assert(this.elems != null);
+ for (int i = 0; i < elems.Length; i++)
n[ct++] = elems[i];
return n;
}
-
+
//ASM Update - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
public Sequence Update(int i, object v) {
- Sequence n = new Sequence(new Capacity(card+1));
- assert this.elems != null;
- assert n.elems != null;
- for (int j = 0; j < elems.Length; j++ )
+ Sequence n = new Sequence(new Capacity(card + 1));
+ Contract.Assert(this.elems != null);
+ Contract.Assert(n.elems != null);
+ for (int j = 0; j < elems.Length; j++)
n.elems[j] = elems[j];
- if (i >= 0 && i < card){
+ if (i >= 0 && i < card) {
n.elems[i] = v;
n.card = card;
return n;
} else if (i == card) {
n.elems[i] = v;
- n.card = card+1;
+ n.card = card + 1;
return n;
} else
throw new Exception("Sequence Update out of range");
@@ -483,49 +597,61 @@ namespace PureCollections { //In place Update (and Remove) and Length - - - - - - - - - - - - - - -
public int Length {
- get{return this.card;}
+ get {
+ return this.card;
+ }
}
- public object this[int index]{
- get{assert this.elems != null; return this.elems[index];}
- set{assert this.elems != null; this.elems[index] = value;}
+ public object this[int index] {
+ get {
+ Contract.Assert(this.elems != null);
+ return this.elems[index];
+ }
+ set {
+ Contract.Assert(this.elems != null);
+ this.elems[index] = value;
+ }
}
- public void Add(object o){
- assert this.elems != null; + public void Add(object o) {
+ Contract.Assert(this.elems != null);
int n = this.elems.Length;
int i = this.card++;
- if (i == n){
- int m = n*2; if (m < 4) m = 4;
- object [] newElems = new object [m];
- for (int j = 0; j < n; j++) newElems[j] = elems[j];
+ if (i == n) {
+ int m = n * 2;
+ if (m < 4)
+ m = 4;
+ object[] newElems = new object[m];
+ for (int j = 0; j < n; j++)
+ newElems[j] = elems[j];
elems = newElems;
}
elems[i] = o;
}
-
- public void AddRange(Sequence! seq){
+
+ public void AddRange(Sequence seq) {
+ Contract.Requires(seq != null);
foreach (object o in seq) {
Add(o);
}
}
-
- public void Remove(){
+
+ public void Remove() {
if (card == 0)
return;
card--;
- }
-
+ }
+
// remove the first occurrence of o from this sequence
public void Remove(Object x) {
if (x == null)
throw new MissingCase();
- assert this.elems != null; + Contract.Assert(this.elems != null);
for (int i = 0; i < card; i++) {
if (x.Equals(elems[i])) {
++i;
while (i < card) {
- elems[i-1] = elems[i];
+ elems[i - 1] = elems[i];
++i;
}
card--;
@@ -534,11 +660,10 @@ namespace PureCollections { }
}
}
-
- public void Truncate(int newLen)
- requires 0 <= newLen && newLen <= Length;
- {
- assert elems != null;
+
+ public void Truncate(int newLen) {
+ Contract.Requires(0 <= newLen && newLen <= Length);
+ Contract.Assert(elems != null);
for (int i = newLen; i < card; i++) {
elems[i] = null;
}
@@ -547,65 +672,77 @@ namespace PureCollections { //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[Pure]
- public override string! ToString() {
- string s ="";
- assert this.elems != null; + public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ string s = "";
+ if (this.elems == null)
+ return "(null)";
+ Contract.Assert(this.elems != null);
if (card > 0 && elems[0] is Char) {
- for(int i =0; i < card ; i++)
- {
+ for (int i = 0; i < card; i++) {
object elem = elems[i];
- if (elem != null) { s +=elem.ToString(); }
+ if (elem != null) {
+ s += elem.ToString();
+ }
}
return s;
} else {
s = "[";
- for(int i =0; i < card-1; i++) {
+ for (int i = 0; i < card - 1; i++) {
object elem = elems[i];
- if (elem != null) { s += elem.ToString()+", "; }
+ if (elem != null) {
+ s += elem.ToString() + ", ";
+ }
}
- if (card > 0)
- {
- object last = elems[card-1];
- if (last != null) { s += last.ToString(); }
+ if (card > 0) {
+ object last = elems[card - 1];
+ if (last != null) {
+ s += last.ToString();
+ }
}
s += "]";
return s;
}
}
//Equality- - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals (object that){
- return that != null && that is Sequence && ((Sequence) this == (Sequence) that);
- }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
- public static bool operator == (Sequence s, Sequence t){
- if ((object)s == (object)t) {
- return true;
- } else if ((object)s == null || (object)t == null) {
- return false;
- }
- if (s.card != t.card) return false;
- assert s.elems != null; - assert t.elems != null; - for(int i = 0; i < s.card; i++)
- if (! Equals(s.elems[i], t.elems[i]))
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ return that != null && that is Sequence && ((Sequence)this == (Sequence)that);
+ }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
+ public static bool operator ==(Sequence s, Sequence t) {
+ if ((object)s == (object)t) {
+ return true;
+ } else if ((object)s == null || (object)t == null) {
+ return false;
+ }
+ if (s.card != t.card)
+ return false;
+ Contract.Assert(s.elems != null);
+ Contract.Assert(t.elems != null);
+ for (int i = 0; i < s.card; i++)
+ if (!Equals(s.elems[i], t.elems[i]))
return false;
- return true; + return true;
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
- public static bool operator != (Sequence s, Sequence t){
- return !(s == t); + [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)] // ugh, is this right? --KRML
+ public static bool operator !=(Sequence s, Sequence t) {
+ return !(s == t);
}
[Pure]
- public override int GetHashCode (){
+ public override int GetHashCode() {
int h = 0;
- for(int i = 0; i < card; i++)
- {
- assert this.elems != null; + for (int i = 0; i < card; i++) {
+ Contract.Assert(this.elems != null);
object elem = elems[i];
- if (elem != null) { h += elem.GetHashCode(); }
+ if (elem != null) {
+ h += elem.GetHashCode();
+ }
}
- return h; + return h;
}
//Subset- - - - - - - - - - - - - - - - - - - - - - - - - - - - -
// View Sequence of T as Set of (Integer,T)
@@ -613,44 +750,57 @@ namespace PureCollections { if (o == null || !(o is Sequence))
throw new MissingCase();
// WS Improve performance!
- Sequence t = (Sequence) o;
- if (this < t) return -1;
- else if(this > t) return +1;
- else return 0;
- }
-
- public static bool operator < (Sequence s, Sequence t){
- if (s==null) throw new ArgumentNullException("s");
- if (t==null) throw new ArgumentNullException("t");
- if (s.card >= t.card) return false;
- assert s.elems != null; - assert t.elems != null; - for(int i = 0; i < s.card; i++)
- if ( ! Equals(s.elems[i], t.elems[i]))
+ Sequence t = (Sequence)o;
+ if (this < t)
+ return -1;
+ else if (this > t)
+ return +1;
+ else
+ return 0;
+ }
+
+ public static bool operator <(Sequence s, Sequence t) {
+ if (s == null)
+ throw new ArgumentNullException("s");
+ if (t == null)
+ throw new ArgumentNullException("t");
+ if (s.card >= t.card)
+ return false;
+ Contract.Assert(s.elems != null);
+ Contract.Assert(t.elems != null);
+ for (int i = 0; i < s.card; i++)
+ if (!Equals(s.elems[i], t.elems[i]))
return false;
- return true; - }
- public static bool operator <= (Sequence s, Sequence t){
- if (s==null) throw new ArgumentNullException("s");
- if (t==null) throw new ArgumentNullException("t");
- if (s.card > t.card) return false;
- assert s.elems != null; - assert t.elems != null; - for(int i = 0; i < s.card; i++)
- if ( ! Equals(s.elems[i], t.elems[i]))
+ return true;
+ }
+ public static bool operator <=(Sequence s, Sequence t) {
+ if (s == null)
+ throw new ArgumentNullException("s");
+ if (t == null)
+ throw new ArgumentNullException("t");
+ if (s.card > t.card)
+ return false;
+ Contract.Assert(s.elems != null);
+ Contract.Assert(t.elems != null);
+ for (int i = 0; i < s.card; i++)
+ if (!Equals(s.elems[i], t.elems[i]))
return false;
- return true; + return true;
+ }
+ public static bool operator >(Sequence s, Sequence t) {
+ return t < s;
+ }
+ public static bool operator >=(Sequence s, Sequence t) {
+ return t <= s;
}
- public static bool operator > (Sequence s, Sequence t){ return t < s;}
- public static bool operator >= (Sequence s, Sequence t){ return t <= s;}
//pure---------------------------------------------------------------
[Pure]
public bool Has(object x) { // WS translate to tailrecursion
if (x == null)
throw new MissingCase();
- assert this.elems != null; - for (int i = 0; i< card; i++)
+ Contract.Assert(this.elems != null);
+ for (int i = 0; i < card; i++)
if (x.Equals(elems[i]))
return true;
return false;
@@ -662,8 +812,8 @@ namespace PureCollections { public int IndexOf(object x) {
if (x == null)
throw new MissingCase();
- assert this.elems != null; - for (int i = 0; i< card; i++)
+ Contract.Assert(this.elems != null);
+ for (int i = 0; i < card; i++)
if (x.Equals(elems[i]))
return i;
return -1;
@@ -675,111 +825,135 @@ namespace PureCollections { public int LastIndexOf(object x) {
if (x == null)
throw new MissingCase();
- assert this.elems != null; + Contract.Assert(this.elems != null);
for (int i = card - 1; i >= 0; i--)
if (x.Equals(elems[i]))
return i;
return -1;
}
- public object Head() {assert this.elems != null; return elems[0]; }
- public object Last() {assert this.elems != null; return elems[card-1]; }
+ public object Head() {
+ Contract.Assert(this.elems != null);
+ return elems[0];
+ }
+ public object Last() {
+ Contract.Assert(this.elems != null);
+ return elems[card - 1];
+ }
- public static Sequence Tail(Sequence! s) {
- Sequence n = new Sequence(new Capacity(s.card-1));
- assert n.elems != null; - assert s.elems != null; - for (int i = 1; i< s.card; i++) n.elems[n.card++] = s.elems[i];
+ public static Sequence Tail(Sequence s) {
+ Contract.Requires(s != null);
+ Sequence n = new Sequence(new Capacity(s.card - 1));
+ Contract.Assert(n.elems != null);
+ Contract.Assert(s.elems != null);
+ for (int i = 1; i < s.card; i++)
+ n.elems[n.card++] = s.elems[i];
return n;
}
- public static Sequence Front(Sequence! s) {
- Sequence n = new Sequence(new Capacity(s.card-1));
- assert n.elems != null; - assert s.elems != null; - for (int i = 0; i< s.card-1; i++) n.elems[n.card++] = s.elems[i];
+ public static Sequence Front(Sequence s) {
+ Contract.Requires(s != null);
+ Sequence n = new Sequence(new Capacity(s.card - 1));
+ Contract.Assert(n.elems != null);
+ Contract.Assert(s.elems != null);
+ for (int i = 0; i < s.card - 1; i++)
+ n.elems[n.card++] = s.elems[i];
return n;
}
- public static Sequence Concat(Sequence! s) {
+ public static Sequence Concat(Sequence s) {
+ Contract.Requires(s != null);
Sequence n = new Sequence(new Capacity(s.card));
- assert n.elems != null; - assert s.elems != null; - for (int i = 0; i< s.card; i++) {
- Sequence t = (Sequence!) s.elems[i];
- assert t.elems != null; - for (int j = 0; j < t.card; j ++)
+ Contract.Assert(n.elems != null);
+ Contract.Assert(s.elems != null);
+ for (int i = 0; i < s.card; i++) {
+ Sequence t = (Sequence)cce.NonNull(s.elems[i]);
+ Contract.Assert(t.elems != null);
+ for (int j = 0; j < t.card; j++)
n.Add(t.elems[j]);
}
return n;
}
- public static Sequence Reverse(Sequence! s) {
+ public static Sequence Reverse(Sequence s) {
+ Contract.Requires(s != null);
Sequence n = new Sequence(new Capacity(s.card));
- assert n.elems != null; - assert s.elems != null; - for (int i = s.card-1; i>=0; i--) n.elems[n.card++] = s.elems[i];
+ Contract.Assert(n.elems != null);
+ Contract.Assert(s.elems != null);
+ for (int i = s.card - 1; i >= 0; i--)
+ n.elems[n.card++] = s.elems[i];
return n;
}
- public static Sequence operator + (Sequence s, Sequence t)
- {
- if (s==null) throw new ArgumentNullException("s");
- if (t == null) throw new ArgumentNullException("t");
- return Append(t,s);
- }
-
- public static Sequence! Append(Sequence! s, Sequence! t) {
- Sequence! n = new Sequence(new Capacity(s.card + t.card));
- assert n.elems != null; - assert s.elems != null; - assert t.elems != null; - for (int i = 0; i< s.card; i++) n.elems[n.card++] = s.elems[i];
- for (int i = 0; i< t.card; i++) n.elems[n.card++] = t.elems[i];
+ public static Sequence operator +(Sequence s, Sequence t) {
+ if (s == null)
+ throw new ArgumentNullException("s");
+ if (t == null)
+ throw new ArgumentNullException("t");
+ return Append(t, s);
+ }
+
+ public static Sequence Append(Sequence s, Sequence t) {
+ Contract.Requires(t != null);
+ Contract.Requires(s != null);
+ Contract.Ensures(Contract.Result<Sequence>() != null);
+ Sequence n = new Sequence(new Capacity(s.card + t.card));
+ Contract.Assert(n != null);
+ Contract.Assert(n.elems != null);
+ Contract.Assert(s.elems != null);
+ Contract.Assert(t.elems != null);
+ for (int i = 0; i < s.card; i++)
+ n.elems[n.card++] = s.elems[i];
+ for (int i = 0; i < t.card; i++)
+ n.elems[n.card++] = t.elems[i];
return n;
}
- public static Sequence Zip(Sequence! s, Sequence! t) {
- int min = s.card<t.card ? s.card : t.card;
+ public static Sequence Zip(Sequence s, Sequence t) {
+ Contract.Requires(t != null);
+ Contract.Requires(s != null);
+ int min = s.card < t.card ? s.card : t.card;
Sequence n = new Sequence(new Capacity(min));
- assert n.elems != null; - assert s.elems != null; - assert t.elems != null; - for (int i = 0; i< min; i++) n.elems[n.card++] = new Tuple(s.elems[i], t.elems[i]);
+ Contract.Assert(n.elems != null);
+ Contract.Assert(s.elems != null);
+ Contract.Assert(t.elems != null);
+ for (int i = 0; i < min; i++)
+ n.elems[n.card++] = new Tuple(s.elems[i], t.elems[i]);
return n;
}
- public static Tuple Unzip(Sequence! s) {
+ public static Tuple Unzip(Sequence s) {
+ Contract.Requires(s != null);
Sequence n0 = new Sequence(new Capacity(s.card));
Sequence n1 = new Sequence(new Capacity(s.card));
- assert s.elems != null; - assert n0.elems != null; - assert n1.elems != null; - for (int i = 0; i< s.card; i++) {
- n0.elems[n0.card++] = ((!)((Tuple!)s.elems[i]).elems)[0];
- n1.elems[n1.card++] = ((!)((Tuple!)s.elems[i]).elems)[1];
+ Contract.Assert(s.elems != null);
+ Contract.Assert(n0.elems != null);
+ Contract.Assert(n1.elems != null);
+ for (int i = 0; i < s.card; i++) {
+ n0.elems[n0.card++] = (cce.NonNull((Tuple)s.elems[i]).elems)[0];
+ n1.elems[n1.card++] = (cce.NonNull((Tuple)s.elems[i]).elems)[1];
}
- return new Tuple(n0,n1);
+ return new Tuple(n0, n1);
}
public static Sequence FromTo(int from, int to) { //WS hash the result!
- if (from > to) return new Sequence();
- Sequence n = new Sequence(new Capacity(to-from+1));
- assert n.elems != null; - for (int i = from; i<= to; i++)
+ if (from > to)
+ return new Sequence();
+ Sequence n = new Sequence(new Capacity(to - from + 1));
+ Contract.Assert(n.elems != null);
+ for (int i = from; i <= to; i++)
n.elems[n.card++] = i;
return n;
}
-
- public static Sequence FromStepTo(int from, int step, int to) {
+
+ public static Sequence FromStepTo(int from, int step, int to) {
Sequence n = new Sequence();
- int incr = step-from;
- if (incr >0)
- for (int i = from; i<= to; i+=incr)
- n.Add(i); + int incr = step - from;
+ if (incr > 0)
+ for (int i = from; i <= to; i += incr)
+ n.Add(i);
else if (incr < 0)
- for (int i = to; i>= from; i-=incr)
- n.Add(i); + for (int i = to; i >= from; i -= incr)
+ n.Add(i);
return n;
}
-
- }
-}
+ }
+}
\ No newline at end of file |