79 It is quite clear that once we made |
79 It is quite clear that once we made |
80 $v$ to align with $\textit{bsimp} \; r_{c}$ |
80 $v$ to align with $\textit{bsimp} \; r_{c}$ |
81 in the inhabitation relation, something different than $v_{r}^{c}$ needs to be plugged |
81 in the inhabitation relation, something different than $v_{r}^{c}$ needs to be plugged |
82 in for the above statement to hold. |
82 in for the above statement to hold. |
83 Ausaf et al. \cite{AusafUrbanDyckhoff2016} |
83 Ausaf et al. \cite{AusafUrbanDyckhoff2016} |
84 made some initial attempts on the un-annotated lexer (to be continued) |
84 made some initial attempts with this idea, see \cite{FahadThesis} |
85 |
85 for details. |
86 |
86 The other route is to dispose of lemma \ref{retrieveStepwise}, |
87 |
87 and prove a slightly weakened inductive invariant instead. |
88 |
88 We adopt this approach in this thesis. |
89 |
89 |
90 From this chapter we start with the main contribution of this thesis, which |
90 We first introduce why the inductive invariant in $\blexer$'s proof |
91 |
91 is too strong, and suggest a few possible fixes, which leads to |
92 o |
92 our proof which we believe was the most natural and effective method. |
93 In particular, the $\blexer$ proof relies on a lockstep POSIX |
93 |
|
94 |
|
95 |
|
96 \section{Why Lemma \ref{retrieveStepwise}'s Requirement is too Strong} |
|
97 |
|
98 %From this chapter we start with the main contribution of this thesis, which |
|
99 |
|
100 The $\blexer$ proof relies on a lockstep POSIX |
94 correspondence between the lexical value and the |
101 correspondence between the lexical value and the |
95 regular expression in each derivative and injection. |
102 regular expression in each derivative and injection. |
96 |
103 If we zoom into the diagram \ref{fig:Inj} and look specifically at |
97 |
104 the pairs $v_i, r_i$ and $v_{i+1} r_{i+1}$, and the invariant of these |
98 which is essential for getting an understanding this thesis |
105 pairs, we get the following correspondence |
99 in chapter \ref{Bitcoded1}, which is necessary for understanding why |
106 |
100 the proof |
107 \begin{tikzpicture}[ |
101 |
108 -{Stealth[scale=1.5]}, % arrow style |
102 In this chapter, |
109 shorten >=1pt, % distance from node to arrow head |
|
110 node distance=2cm, |
|
111 font=\sffamily |
|
112 ] |
|
113 |
|
114 \matrix (M) [matrix of nodes, nodes in empty cells, column sep=2cm, row sep=2cm, |
|
115 nodes={execute at begin node=\phantom}] |
|
116 { |
|
117 1 & {$b_{s}(a_{0}+a_{1a})^{*}$} & 3 & 4\\ |
|
118 5 & 6 & 7 & 8\\ |
|
119 9 & 10 & 11 & 12\\ |
|
120 }; |
|
121 |
|
122 \foreach \i in {2,...,3} % go through each column |
|
123 \draw[dotted] (M-1-\i) -- (M-2-\i) -- (M-3-\i); |
|
124 |
|
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 % |
|
130 % |
|
131 %which is essential for getting an understanding this thesis |
|
132 %in chapter \ref{Bitcoded1}, which is necessary for understanding why |
|
133 %the proof |
|
134 % |
|
135 %In this chapter, |
103 |
136 |
104 %We contrast our simplification function |
137 %We contrast our simplification function |
105 %with Sulzmann and Lu's, indicating the simplicity of our algorithm. |
138 %with Sulzmann and Lu's, indicating the simplicity of our algorithm. |
106 %This is another case for the usefulness |
139 %This is another case for the usefulness |
107 %and reliability of formal proofs on algorithms. |
140 %and reliability of formal proofs on algorithms. |