6 \label{Bitcoded2} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX} |
6 \label{Bitcoded2} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX} |
7 %Then we illustrate how the algorithm without bitcodes falls short for such aggressive |
7 %Then we illustrate how the algorithm without bitcodes falls short for such aggressive |
8 %simplifications and therefore introduce our version of the bitcoded algorithm and |
8 %simplifications and therefore introduce our version of the bitcoded algorithm and |
9 %its correctness proof in |
9 %its correctness proof in |
10 %Chapter 3\ref{Chapter3}. |
10 %Chapter 3\ref{Chapter3}. |
|
11 {\color{red} \rule{\linewidth}{0.5mm}} |
|
12 New content starts. |
|
13 {\color{red} \rule{\linewidth}{0.5mm}} |
|
14 |
11 \section{Overview} |
15 \section{Overview} |
12 |
16 |
13 This chapter |
17 This chapter |
14 is the point from which novel contributions of this PhD project are introduced |
18 is the point from which novel contributions of this PhD project are introduced |
15 in detail, |
19 in detail, |
98 %From this chapter we start with the main contribution of this thesis, which |
102 %From this chapter we start with the main contribution of this thesis, which |
99 |
103 |
100 The $\blexer$ proof relies on a lockstep POSIX |
104 The $\blexer$ proof relies on a lockstep POSIX |
101 correspondence between the lexical value and the |
105 correspondence between the lexical value and the |
102 regular expression in each derivative and injection. |
106 regular expression in each derivative and injection. |
103 If we zoom into the diagram \ref{fig:Inj} and look specifically at |
107 If we zoom into the diagram \ref{graph:in} and look specifically at |
104 the pairs $v_i, r_i$ and $v_{i+1} r_{i+1}$, and the invariant of these |
108 the pairs $v_i, r_i$ and $v_{i+1},\, r_{i+1}$, we get the diagram demonstrating |
105 pairs, we get the following correspondence |
109 the invariant that the same bitcodes can be extracted from the pairs: |
106 |
110 |
107 \begin{tikzpicture}[ |
111 When simplifications are added, the inhabitation relation no longer holds, |
108 -{Stealth[scale=1.5]}, % arrow style |
112 causing the above diagram to break. |
109 shorten >=1pt, % distance from node to arrow head |
113 |
110 node distance=2cm, |
114 Ausaf addressed this with an augmented lexer he called $\textit{slexer}$. |
111 font=\sffamily |
115 |
112 ] |
116 |
113 |
117 |
114 \matrix (M) [matrix of nodes, nodes in empty cells, column sep=2cm, row sep=2cm, |
118 we note that the invariant |
115 nodes={execute at begin node=\phantom}] |
119 $\vdash v_{i+1}: r_{i+1} \implies \retrieve \; r_{i+1} \; v_{i+1} $ is too strong |
116 { |
120 to maintain because the precondition $\vdash v_i : r_i$ is too weak. |
117 1 & {$b_{s}(a_{0}+a_{1a})^{*}$} & 3 & 4\\ |
121 It does not require $v_i$ to be a POSIX value |
118 5 & 6 & 7 & 8\\ |
122 |
119 9 & 10 & 11 & 12\\ |
123 |
120 }; |
124 {\color{red} \rule{\linewidth}{0.5mm}} |
121 |
125 New content ends |
122 \foreach \i in {2,...,3} % go through each column |
126 {\color{red} \rule{\linewidth}{0.5mm}} |
123 \draw[dotted] (M-1-\i) -- (M-2-\i) -- (M-3-\i); |
127 |
124 |
128 |
125 \foreach \i in {1,2} % go through each row |
|
126 \draw[->] (M-\i-2.east) -- (M-\i-3.west); |
|
127 \end{tikzpicture} |
|
128 |
129 |
129 % |
130 % |
130 % |
131 % |
131 %which is essential for getting an understanding this thesis |
132 %which is essential for getting an understanding this thesis |
132 %in chapter \ref{Bitcoded1}, which is necessary for understanding why |
133 %in chapter \ref{Bitcoded1}, which is necessary for understanding why |