2002-09-13 Nick Drochak <ndrochak@gol.com>

[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 603448b0f22b0be6a8d0e05d8f383bce223fbc1f..7689a5a3b4ce1e2386295460c20c910dee636d9e 100644 (file)
--- a/mcs/class/corlib/System/CharEnumerator.cs
+++ b/mcs/class/corlib/System/CharEnumerator.cs
@@ -10,58 +10,81 @@ using System.Collections;
 
 namespace System
 {
-          [Serializable]
-          public sealed class CharEnumerator : IEnumerator, ICloneable
-          {
-                private string str;
-                private int idx;
-                        
-           // Constructor
-                internal CharEnumerator (string s)
-                {
-                           str = s;
-                           idx = -1;
-                }
-                        
-                // Property
-                public char Current
-                {
-                           get {
-                                 if (idx == -1)
-                                               throw new InvalidOperationException ("The position is not valid.");
-                                                                                 
-                                 return str[idx];
-                           }
-                }
+       [Serializable]
+       public sealed class CharEnumerator : IEnumerator, ICloneable
+       {
+               private string str;
+               private int index;
+               private int length;
+               // Representation invariant:
+               // length == str.Length
+               // -1 <= index <= length
+               
+               // Constructor
+               internal CharEnumerator (string s)
+               {
+                        str = s;
+                        index = -1;
+                        length = s.Length;
+               }
+               
+               // Property
+               public char Current
+               {
+                       get {
+                               if (index == -1 || index == length)
+                                       throw new InvalidOperationException
+                                               ("The position is not valid.");
 
-                object IEnumerator.Current {
-                           get {
-                                         if (idx == -1)
-                                                       throw new InvalidOperationException ("The position is not valid");
-                                         return str [idx];
-                           }
-                }
-                        
-                // Methods
-                public object Clone ()
-                {
-                           CharEnumerator x = new CharEnumerator (str);
-                           x.idx = idx;
-                           return x;
-                }
-                        
-                public bool MoveNext ()
-                {
-                           if (idx > str.Length) {
-                                         idx = -1;
-                                         return false;
-                           } else
-                                         return true;
-                }
-                        
-                public void Reset ()
-                {
-                           idx = 0;
-                }
-   }
+                               return str [index];
+                       }
+               }
+               
+               object IEnumerator.Current
+               {
+                       get {
+                               if (index == -1 || index == length)
+                                       throw new InvalidOperationException
+                                               ("The position is not valid");
+
+                               return str [index];
+                       }
+               }
+               
+               // Methods
+               public object Clone ()
+               {
+                       CharEnumerator x = new CharEnumerator (str);
+                       x.index = index;
+                       return x;
+               }
+               
+               public bool MoveNext ()
+               {
+                       // Representation invariant holds: -1 <= index <= length
+
+                       index ++;
+
+                       // Now: 0 <= index <= length+1;
+                       //   <=>
+                       // 0 <= index < length (OK) || 
+                       // length <= index <= length+1 (Out of bounds)
+                       
+                       if (index >= length) {
+                               index = length;
+                               // Invariant restored:
+                               // length == index
+                               //   =>
+                               // -1 <= index <= length
+                               return false;   
+                       }
+                       else
+                               return true;
+               }
+               
+               public void Reset ()
+               {
+                       index = -1;
+               }
+       }
 }