Index: doc/theses/jiada_liang_MMath/CFAenum.tex
===================================================================
--- doc/theses/jiada_liang_MMath/CFAenum.tex	(revision 29c8675099308007aaa5be2a10db2bc13c6dbca7)
+++ doc/theses/jiada_liang_MMath/CFAenum.tex	(revision d93b8131b6d6f864fdf457bb174840310cb9dfd1)
@@ -147,5 +147,15 @@
 const T E_values [3] = { t1, t2, t3 };
 \end{cfa}
-The generated C enumeration will have enumerator values equals to their positions thanks to C's auto-initialization scheme. Notice that value and label arrays are dynamically allocated data structures that take up 
+The generated C enumeration will have enumerator values resemble \CFA enumerator positions thanks to C's auto-initialization scheme.
+A \CFA enumeration variable definition is same in \CFA and C, before or after the transpilation.
+For example:
+\begin{cfa}
+enum E e = E1;
+e;
+\end{cfa}
+These two expressions will not change by \CFA-cc. A \CFA enumeration variable will always have the same underlying representation as its generated 
+C enumeration. This implies \CFA enumeration variable does not take up extra memory and \CFA enumeration use @posn@ as its underlying representation.
+
+Notice that value and label arrays are dynamically allocated data structures that take up 
 memory. If an enumeration is globally defined, the arrays are allocated in the @.data@ section and will be initialized before the program execution.
 Otherwise, if an enumeration has its definition in a local scope, these arrays will be allocated on the stack and be initialized when the program counter 
@@ -212,5 +222,5 @@
 
 
-\section{Auto Initialization}
+\section{Initialization}
 \CFA extends C's auto-initialization scheme to \CFA enumeration. For an enumeration type with base type T, the initialization scheme is the following:
 \begin{enumerate}
Index: doc/theses/jiada_liang_MMath/conclusion.tex
===================================================================
--- doc/theses/jiada_liang_MMath/conclusion.tex	(revision 29c8675099308007aaa5be2a10db2bc13c6dbca7)
+++ doc/theses/jiada_liang_MMath/conclusion.tex	(revision d93b8131b6d6f864fdf457bb174840310cb9dfd1)
@@ -71,6 +71,103 @@
 Label arrays are auxiliary data structures that are always generated for \CFA enumeration, which is a considerable program overhead. 
 It is helpful to provide a new syntax or annotation for a \CFA enumeration definition that tells the compiler the labels will not be used 
-throughout the execution. Therefore, \CFA optimizes the label array away. The @value()@ function can still be used on an enumeration constant, 
-and the function called is reduced to a @char *@ constant expression that holds the name of the enumerator. But if @value()@ is called on 
+throughout the execution. Therefore, \CFA optimizes the label array away. The @label()@ function can still be used on an enumeration constant, 
+and the function called is reduced to a @char *@ constant expression that holds the name of the enumerator. But if @label()@ is called on 
 a variable with an enumerated type, it returns an empty string since the label information is lost for the runtime.
+\item
+\CFA enumeration has its limitation in separate compilation. Consider the followings example:
+\begin{cfa}
+// libvacodec.h: v1
+enum(int) C_Codec ! {
+    FIRST_VIDEO = 0,
+    VP8 = 2,
+    VP9 = 4,
+    LAST_VIDEO = 8,
+
+    FIRST_AUDIO = 3,
+    VORBIS = 9,
+    OPUS = 27,
+    LAST_AUDIO = 81
+};
+
+enum(int) CFA_Codec ! {
+    FIRST_VIDEO = 0,
+    VP8 = 2,
+    VP9 = 4,
+    LAST_VIDEO = 8,
+
+    FIRST_AUDIO = 3,
+    VORBIS = 9,
+    OPUS = 27,
+    LAST_AUDIO = 81
+};
+
+// main.c
+C_Codec c_code = C_Codec.VORBIS;
+CFA_Codec cfa_code = CFA_Codec.VORBIS;
+\end{cfa}
+In the preceding example, the memory location of @c_code@ stores a value 9, the integral value of VORBIS. 
+The memory of @cfa_code@ stores 5, which is the position of @CFA_Codec.VORBIS@ and can be mapped to value 9.
+
+If to insert a new enumerator in both @C_Codec@ and @CFA_Codec@ 
+before the relative position of VORBIS, without a re-compilation of @main.c@, variable @cfa_code@ would be mapped 
+to an unintented value.
+// libvacodec.h: v2
+enum(int) C_Codec ! {
+    FIRST_VIDEO = 0,
+    VP8 = 2,
+    VP9 = 4,
+    @AV1@,
+    LAST_VIDEO = 8,
+
+    FIRST_AUDIO = 3,
+    VORBIS = 9,
+    OPUS = 27,
+    LAST_AUDIO = 81
+};
+
+enum(int) CFA_Codec ! {
+    FIRST_VIDEO = 0,
+    VP8 = 2,
+    VP9 = 4,
+    @AV1@,
+    LAST_VIDEO = 8,
+
+    FIRST_AUDIO = 3,
+    VORBIS = 9,
+    OPUS = 27,
+    LAST_AUDIO = 81
+};
+
+\end{cfa}
+While @c_code@ still has the correct value of 9, @cfa_code@ (5) is now mapped to @First_AUDIO@. In other words, it is 
+necessary to to recompile @main.c@ when to update @libvacodec.h@. 
+
+To avoid a recompilation, enumeration positions can be represented as @extern const@. For example, \CFA-cc can generate the following code for @CFA_Codec@: 
+\begin{cfa}
+// CFA-cc transpile: libvacodec.h
+const int FIRST_VIDEO = 0;
+const int VP8 = 1;
+const int VP9 = 2;
+const int LAST_VIDEO = 3;
+const int FIRST_AUDIO = 4;
+const int VORBIS = 5;
+const int OPUS = 6;
+const int LAST_AUDIO = 7;
+
+// CFA-cc transpile: main.c
+extern const int FIRST_VIDEO;
+extern const int VP8;
+extern const int VP9;
+extern const int LAST_VIDEO;
+extern const int FIRST_AUDIO;
+extern const int VORBIS;
+extern const int OPUS;
+extern const int LAST_AUDIO;
+
+int cfa_code = VORBIS;
+\end{cfa}
+If later a position of an enumerator is changed, the generated expression @int cfa_code = VORBIS;@ will still have the correct 
+value, because it is linked to a external constant @VORBIS@ from @libvacodec.h@. This implementation requires extra memory to store position, but 
+solve the separate compilation problem. 
+
 \end{enumerate}