2002-06-27 Martin Baulig <martin@gnome.org>

[mono.git] / mcs / class / corlib / System / CharEnumerator.cs

diff --git a/mcs/class/corlib/System/CharEnumerator.cs b/mcs/class/corlib/System/CharEnumerator.cs
index c320482c35717548469260794d42a13965cd1bc2..7689a5a3b4ce1e2386295460c20c910dee636d9e 100644 (file)
--- a/mcs/class/corlib/System/CharEnumerator.cs
+++ b/mcs/class/corlib/System/CharEnumerator.cs
@@ -14,33 +14,40 @@ namespace System
        public sealed class CharEnumerator : IEnumerator, ICloneable
        {
                private string str;
-               private int idx;
-               private int len;
+               private int index;
+               private int length;
+               // Representation invariant:
+               // length == str.Length
+               // -1 <= index <= length
                
                // Constructor
                internal CharEnumerator (string s)
                {
                         str = s;
-                        idx = -1;
-                        len = s.Length;
+                        index = -1;
+                        length = s.Length;
                }
                
                // Property
                public char Current
                {
-                       get { if (idx == -1)
-                               throw new InvalidOperationException ("The position is not valid.");
+                       get {
+                               if (index == -1 || index == length)
+                                       throw new InvalidOperationException
+                                               ("The position is not valid.");
 
-                       return str [idx];
+                               return str [index];
                        }
                }
                
                object IEnumerator.Current
                {
-                       get { if (idx == -1)
-                               throw new InvalidOperationException ("The position is not valid");
+                       get {
+                               if (index == -1 || index == length)
+                                       throw new InvalidOperationException
+                                               ("The position is not valid");
 
-                       return str [idx];
+                               return str [index];
                        }
                }
                
@@ -48,29 +55,36 @@ namespace System
                public object Clone ()
                {
                        CharEnumerator x = new CharEnumerator (str);
-                       x.idx = idx;
+                       x.index = index;
                        return x;
                }
                
                public bool MoveNext ()
                {
-                       if (len < 0)
-                               return false;
-                       
-                       idx++;
+                       // Representation invariant holds: -1 <= index <= length
+
+                       index ++;
+
+                       // Now: 0 <= index <= length+1;
+                       //   <=>
+                       // 0 <= index < length (OK) || 
+                       // length <= index <= length+1 (Out of bounds)
                        
-                       if (idx > len) {
-                               idx = -2;
-                               return false;
+                       if (index >= length) {
+                               index = length;
+                               // Invariant restored:
+                               // length == index
+                               //   =>
+                               // -1 <= index <= length
+                               return false;   
                        }
-                       
-                       return true;
+                       else
+                               return true;
                }
                
                public void Reset ()
                {
-                       idx = -1;
-
+                       index = -1;
                }
        }
 }