From 4092e09c042de2999e2bf7718a101d80d5e2d752 Mon Sep 17 00:00:00 2001
From: Michael Stevens
I1 it1I1 it*it1*itT.*it1 = t*it = tI1 is mutable.it1->mit->mT is a type for which t.m is
defined.++ it1++ itI1 &it1 ++it ++I1-- it1-- itI1 &it1 --it --I1it1.index1 ()it.index1 ()C::size_typeit1.index2 ()it.index2 ()C::size_typeit1.begin ()it.begin ()I2it1.end ()it.end ()I2it1.rbegin ()it.rbegin ()reverse_iterator<I2>it1.rend ()it.rend ()reverse_iterator<I2>I1 it1I1 itit1 is singular.it is singular.*it1it1 is dereferenceable.*itit is dereferenceable.*it1 = t*it1.*it = t*it.*it1 is a copy of t.*it is a copy of t.it1->mit1 is dereferenceable.(*it1).mit->mit is dereferenceable.(*it).m++ it1it1 is dereferenceable.it1 is modified to point to the next element of
+++ itit is dereferenceable.it is modified to point to the next element of
the column/row, i.e. for column iterators holdsit1.index1 () < (++ it1).index1 () andit1.index2 () == (++ it1).index2 (),it.index1 () < (++ it).index1 () andit.index2 () == (++ it).index2 (),it1.index1 () == (++ it1).index1 () andit1.index2 () < (++ it1).index2 ().it1 is dereferenceable or past-the-end.
+it.index1 () == (++ it).index1 () andit.index2 () < (++ it).index2 ().it is dereferenceable or past-the-end.
-&it1 == &++ it1.it11 == it12,++ it11 == ++ it12.it1 == it2,++ it1 == ++ it2.
it1 ++++ it1.it ++++ it.{
- I1 it1t = it1;
- ++ it1;
- return it1t;
+ I1 itt = it;
+ ++ it;
+ return itt;
}it1 is dereferenceable or past-the-end.it is dereferenceable or past-the-end.-- it1it1 is dereferenceable or past-the-end.it1t such that
-it1 == ++ it1t.it1 is modified to point to the previous
+-- itit is dereferenceable or past-the-end.itt such that
+it == ++ itt.it is modified to point to the previous
element of the column/row, i.e. for column iterators holdsit1.index1 () > (-- it1).index1 () andit1.index2 () == (-- it1).index2 (),it.index1 () > (-- it).index1 () andit.index2 () == (-- it).index2 (),it1.index1 () == (-- it1).index1 () andit1.index2 () > (-- it1).index2 ().it1 is dereferenceable.&it1 = &-- it1.it11 == it12,-- it11 == -- it12.it.index1 () == (-- it).index1 () andit.index2 () > (-- it).index2 ().
+it is dereferenceable.&it = &-- it.it1 == it2,-- it1 == -- it2.it1 --it1.it --it.{
- I1 it1t = it1;
- -- it1;
- return it1t;
+ I1 itt = it;
+ -- it;
+ return itt;
}it1 is dereferenceable. it is dereferenceable. it1.index1 ()it1 is dereferenceable.it1.index1 () >= 0 andit1.index1 () < it () .size1 ()it11 == it12,it11.index1 () == it12.index1 ()
-.it11, it12 are Indexed Bidirectional
-Row Iterators with it11 == it12,it11.index1 () < (++ it12).index1
-().it11, it12 are Indexed Bidirectional
-Row Iterators with it11 == it12,it11.index1 () > (-- it12).index1
-().it.index1 ()it is a Row iterator then it must be dereferenceable.it.index1 () >= 0 andit.index1 () < it () .size1 ()it1 == it2,it1.index1 () == 12.index1 ().it1, it2 are Row Iterators with it1 == it2,it1.index1 () < (++ it2).index1 ().it1.index1 () > (-- it2).index1 ().it1.index2 ()it1 is dereferenceable.it1.index2 () >= 0 andit1.index2 () < it () .size2 ()it11 == it12,it11.index2 () == it12.index2 ()
+it.index2 ()it is a Column iterator then it must be dereferenceable.it.index2 () >= 0 andit.index2 () < it () .size2 ()it1 == it2,it1.index2 () == it2.index2 ()
.it11, it12 are Indexed Bidirectional
-Column Iterators with it11 == it12,it11.index2 () < (++ it12).index2
-().it11, it12 are Indexed Bidirectional
-Column Iterators with it11 == it12,it11.index2 () > (-- it12).index2
-().it1, it2 are Column Iterators with it1 == i12,it1.index2 () < (++ it2).index2 ().it1.index2 () > (-- it2).index2 ().
it1.begin ()it1 is dereferenceable.it1 is a Indexed Bidirectional Column
-Iterator,it2 = it1.begin () is a Indexed Bidirectional Row
-Iteratorit2.index1 () == it1.index1 ().
-If it1 is a Indexed Bidirectional Row
-Iterator,
-then it2 = it1.begin () is a Indexed Bidirectional
-Column Iterator
-with it2.index2 () == it1.index2 ().
it.begin ()it is dereferenceable.it is a Column Iterator,it2 = it.begin () is a Row Iteratorit2.index1 () == it.index1 ().
+If it is a Row Iterator,
+then it2 = it.begin () is a Column Iterator
+with it2.index2 () == it.index2 ().
it1.end ()it1 is dereferenceable.it1 is a Indexed Bidirectional Column
-Iterator,it2 = it1.end () is a Indexed Bidirectional Row
-Iteratorit2.index1 () == it1.index1 ().
-If it1 is a Indexed Bidirectional Row
-Iterator,
-then it2 = it1.end () is a Indexed Bidirectional
-Column Iterator
-with it2.index2 () == it1.index2 ().
it.end ()it is dereferenceable.it is a Column Iterator,it2 = it.end () is a Row Iteratorit2.index1 () == it.index1 ().
+If it is a Row Iterator,
+then it2 = it.end () is a Column Iterator
+with it2.index2 () == it.index2 ().
it1.rbegin ()it1 is dereferenceable.reverse_iterator<I2> (it1.end
+it.rbegin ()
+it is dereferenceable.
+Equivalent to reverse_iterator<I2> (it.end
()).
it1.rend ()it1 is dereferenceable.reverse_iterator<I2> (it1.begin
+it.rend ()
+it is dereferenceable.
+Equivalent to reverse_iterator<I2> (it.begin
()).
it11 == it12 if and only if &*it11 ==
-&*it12.it1 == it2 if and only if &*it1 ==
+&*it2.it1 is dereferenceable, then ++ it1;
---it1; is a null operation. Similarly, -- it1; ++
-it1; is a null operation.it is dereferenceable, then ++ it;
+--it; is a null operation. Similarly, -- it; ++
+it; is a null operation.it1 is dereferenceable, *it1 == it1 ()
-(it1.index1 (), it2.index2 ())it is dereferenceable, *it == it ()
+(it.index1 (), it.index2 ())it1 is a Indexed Bidirectional Column Iterator
-and it2 = it1.begin () then it2.index2 () <
+If it is a Column Iterator
+and it2 = it.begin () then it2.index2 () <
it2t.index2 () for all it2t with it2t ()
== it2 () and it2t ().index1 () == it2 ().index1
().
-If it1 is a Indexed Bidirectional Row Iterator and
-it2 = it1.begin () then it2.index1 () <
+If it is a Row Iterator and
+it2 = it.begin () then it2.index1 () <
it2t.index1 () for all it2t with it2t ()
== it2 () and it2t ().index2 () == it2 ().index2
().
@@ -923,13 +904,13 @@ it2t.index1 () for all it2t with it2t ()
Relation between iterator column/row end and iterator
index
-If it1 is a Indexed Bidirectional Column Iterator
-and it2 = it1.end () then it2.index2 () >
+If it is a Column Iterator
+and it2 = it.end () then it2.index2 () >
it2t.index2 () for all it2t with it2t ()
== it2 () and it2t ().index1 () == it2 ().index1
().
-If it1 is a Indexed Bidirectional Row Iterator and
-it2 = it1.end () then it2.index1 () >
+If it is a Row Iterator and
+it2 = it.end () then it2.index1 () >
it2t.index1 () for all it2t with it2t ()
== it2 () and it2t ().index2 () == it2 ().index2
().