Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 5c27b6ad08917d58f58d765b5c89f0491e326a39)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision de3a579300a8b9d3a7728dab02abe44c972da598)
@@ -229,5 +229,5 @@
 \end{tabular}
 \end{cquote}
-Here, the intuitive code on the left is implicitly transformed into the statndard implementation on the right, using the value of the enumeration variable and enumerators.
+Here, the intuitive code on the left is implicitly transformed into the standard implementation on the right, using the value of the enumeration variable and enumerators.
 However, this implementation is fragile, \eg if the enumeration is changed to:
 \begin{cfa}
@@ -316,2 +316,88 @@
 \label{f:PlanetExample}
 \end{figure}
+
+\section{Enum Trait}
+A typed enum comes with traits capture enumeration charastics and helper functions. 
+
+\begin{cfa}
+forall(E) trait Bounded {
+	E lowerBound();
+	E upperBound();
+};
+\end{cfa}
+\CFA enums satisfy Bounded trait thanks to the compiler implementing lowerBound() and upperBound(), with 
+lowerBound() returning the first enumerator and upperBound() return the last.
+
+\begin{cfa}
+Workday day1 = lowerBound(); // Monday
+Planet lastPlanet = upperBound(); // NEPTUNE
+\end{cfa}
+
+Because lowerBound() and upperBound() are overloaded with return types only, calling either functions 
+in a null context cause type ambiguity if than one type implementing Bounded traits, including typed enumerations.
+\begin{cfa}
+Workday day1 = lowerBound(); // Okay because rhs hints lowerBound() to return a Workday
+void foo(Planet p);
+foo( upperBound() ); Okay because foo's parameter give type hint
+// lowerBound(); // Error because both Planet and Workday implements Bounded
+\end{cfa}
+
+\begin{cfa}
+forall(E | Bounded(E)) trait Serial {
+	unsigned fromInstance(E e);
+	E fromInt(unsigned i);
+	E succ(E e);
+	E pred(E e);
+};
+\end{cfa}
+A Serial type can be mapped to a sequnce of integer. For enum types, fromInstance(E e) is equivalent to 
+posE(E e). Enumerations implement fromInt(), succ(), and pred() with bound() check.
+For an enum declares N enumerators, fromInt(i) returns the ith enumerator of type E if $0 \leq i < N$.
+If e is the i-th enumerator, succ(e) returns the i+1-th enumerator if $e != upperBound()$ and pred(e) 
+returns the i-1-th enumerator $e != lowerBound()$. \CFA compile gives an error if bound check fails.
+
+\begin{cfa}
+forall(E, T) trait TypedEnum {
+	T valueE(E e);
+	char * labelE(E e);
+	unsigned int posE(E e);
+};
+\end{cfa}
+
+The TypedEnum trait capture three basic attributes of type enums. TypedEnum asserts two types E and T, with T being the base type of enumeration E.
+With an assertion on TypedEnum, we can implement functions for all type enums.
+
+\begin{cfa}
+forall( E, T | TypeEnum(E, T))
+void printEnum(E e) {
+	sout | "Enum "| labelE(e);
+}
+printEunm(MARS);
+\end{cfa}
+
+@<enum.hfa>@ overwrites comparison operators for type enums. 
+\begin{cfa}
+forall(E, T| TypedEnum(E, T)) {
+	// comparison
+	int ?==?(E l, E r);
+	int ?!=?(E l, E r);
+	int ?!=?(E l, zero_t);
+	int ?<?(E l, E r);
+	int ?<=?(E l, E r);
+	int ?>?(E l, E r);
+	int ?>=?(E l, E r);
+}
+\end{cfa}
+These overloaded operators are not defined if the file is not included.
+In this case, the compiler converts an enumerator to its value, and applies the operators
+if they are defined for the value type T.
+
+\begin{cfa}
+// if not include <enum.hfa>
+enum(int) Fruits {
+	APPLE = 2, BANANA=1, CHERRY=2
+};
+APPLE == CHERRY; // True because they have the same Value
+#include <enum.hfa>
+APPLE == CHERRY; // False because they are different enumerator
+\end{cfa}