33 |
56 |
34 \end{frame} |
57 \end{frame} |
35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
36 |
59 |
37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
61 \begin{frame}[c] |
|
62 \frametitle{Compilers \& Boeings 777} |
|
63 |
|
64 First flight in 1994. They want to achieve triple redundancy in hardware |
|
65 faults.\bigskip |
|
66 |
|
67 They compile 1 Ada program to\medskip |
|
68 |
|
69 \begin{itemize} |
|
70 \item Intel 80486 |
|
71 \item Motorola 68040 (old Macintosh's) |
|
72 \item AMD 29050 (RISC chips used often in laser printers) |
|
73 \end{itemize}\medskip |
|
74 |
|
75 using 3 independent compilers.\bigskip\pause |
|
76 |
|
77 \small Airbus uses C and static analysers. Recently started using CompCert. |
|
78 |
|
79 \end{frame} |
|
80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
81 |
|
82 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
83 \begin{frame}[c] |
|
84 \frametitle{seL4 / Isabelle} |
|
85 |
|
86 \begin{itemize} |
|
87 \item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip |
|
88 \item US DoD has competitions to hack into drones; they found that the |
|
89 isolation guarantees of seL4 hold up\bigskip |
|
90 \item CompCert and seL4 sell their code |
|
91 \end{itemize} |
|
92 |
|
93 \end{frame} |
|
94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
95 |
|
96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
97 \begin{frame}[c] |
|
98 \frametitle{POSIX Matchers} |
|
99 |
|
100 \begin{itemize} |
|
101 \item Longest match rule (``maximal munch rule''): The |
|
102 longest initial substring matched by any regular expression |
|
103 is taken as the next token. |
|
104 |
|
105 \begin{center} |
|
106 \bl{$\texttt{\Grid{iffoo\VS bla}}$} |
|
107 \end{center}\medskip |
|
108 |
|
109 \item Rule priority: |
|
110 For a particular longest initial substring, the first regular |
|
111 expression that can match determines the token. |
|
112 |
|
113 \begin{center} |
|
114 \bl{$\texttt{\Grid{if\VS bla}}$} |
|
115 \end{center} |
|
116 \end{itemize}\bigskip\pause |
|
117 |
|
118 \small |
|
119 \hfill Kuklewicz: most POSIX matchers are buggy\\ |
|
120 \footnotesize |
|
121 \hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix} |
|
122 |
|
123 \end{frame} |
|
124 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
125 |
|
126 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
127 \begin{frame}[c] |
|
128 \mbox{}\\[-14mm]\mbox{} |
|
129 \small |
|
130 \bl{ |
|
131 \begin{center} |
|
132 \begin{tabular}{lcl} |
|
133 $\textit{der}\;c\;(\ZERO)$ & $\dn$ & $\ZERO$\\ |
|
134 $\textit{der}\;c\;(\ONE)$ & $\dn$ & $\ZERO$\\ |
|
135 $\textit{der}\;c\;(d)$ & $\dn$ & $\textit{if}\; c = d\;\textit{then} \;\ONE \; \textit{else} \;\ZERO$\\ |
|
136 $\textit{der}\;c\;(r_1 + r_2)$ & $\dn$ & $(\textit{der}\;c\;r_1) + (\textit{der}\;c\;r_2)$\\ |
|
137 $\textit{der}\;c\;(r_1 \cdot r_2)$ & $\dn$ & $\textit{if}\;\textit{nullable}(r_1)$\\ |
|
138 & & $\textit{then}\;((\textit{der}\;c\;r_1)\cdot r_2) + (\textit{der}\;c\;r_2)$\\ |
|
139 & & $\textit{else}\;(\textit{der}\;c\;r_1)\cdot r_2$\\ |
|
140 $\textit{der}\;c\;(r^*)$ & $\dn$ & $(\textit{der}\;c\;r)\cdot (r^*)$\\ |
|
141 $\textit{der}\;c\;(r^{\{n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\ |
|
142 & & \textit{else if} $\textit{nullable}(r)$ \textit{then} $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\ |
|
143 & & \textit{else} $(\textit{der}\;c\;r)\cdot (r^{\{n-1\}})$\\ |
|
144 $\textit{der}\;c\;(r^{\{\uparrow n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\ |
|
145 & & \textit{else} |
|
146 $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\ |
|
147 \end{tabular} |
|
148 \end{center}} |
|
149 |
|
150 \end{frame} |
|
151 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
152 |
|
153 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
154 \begin{frame}[t] |
|
155 \frametitle{Proofs about Rexps} |
|
156 |
|
157 Remember their inductive definition: |
|
158 |
|
159 \begin{center} |
|
160 \begin{tabular}{@ {}rrl} |
|
161 \bl{$r$} & \bl{$::=$} & \bl{$\ZERO$}\\ |
|
162 & \bl{$\mid$} & \bl{$\ONE$} \\ |
|
163 & \bl{$\mid$} & \bl{$c$} \\ |
|
164 & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\ |
|
165 & \bl{$\mid$} & \bl{$r_1 + r_2$} \\ |
|
166 & \bl{$\mid$} & \bl{$r^*$} \\ |
|
167 & \bl{$\mid$} & \bl{$r^{\{n\}}$} \\ |
|
168 & \bl{$\mid$} & \bl{$r^{\{\uparrow n\}}$} \\ |
|
169 \end{tabular} |
|
170 \end{center} |
|
171 |
|
172 If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots |
|
173 |
|
174 \end{frame} |
|
175 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
176 |
|
177 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
178 \begin{frame}[c] |
|
179 \frametitle{Proofs about Rexp (2)} |
|
180 |
|
181 \begin{itemize} |
|
182 \item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip |
|
183 \item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already |
|
184 holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip |
|
185 \item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already |
|
186 holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip |
|
187 \item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already |
|
188 holds for \bl{$r$}. |
|
189 \item \ldots |
|
190 \end{itemize} |
|
191 |
|
192 \end{frame} |
|
193 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
194 |
|
195 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
196 \begin{frame}[c] |
|
197 \frametitle{Proofs about Strings} |
|
198 |
|
199 If we want to prove something, say a property \bl{$P(s)$}, for all |
|
200 strings \bl{$s$} then \ldots\bigskip |
|
201 |
|
202 \begin{itemize} |
|
203 \item \bl{$P$} holds for the empty string, and\medskip |
|
204 \item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$} |
|
205 already holds for \bl{$s$} |
|
206 \end{itemize} |
|
207 \end{frame} |
|
208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
209 |
|
210 |
|
211 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
212 %\begin{frame}[c] |
|
213 % |
|
214 %\bl{\begin{center} |
|
215 %\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} |
|
216 %$zeroable(\varnothing)$ & $\dn$ & \textit{true}\\ |
|
217 %$zeroable(\epsilon)$ & $\dn$ & \textit{false}\\ |
|
218 %$zeroable (c)$ & $\dn$ & \textit{false}\\ |
|
219 %$zeroable (r_1 + r_2)$ & $\dn$ & $zeroable(r_1) \wedge zeroable(r_2)$ \\ |
|
220 %$zeroable (r_1 \cdot r_2)$ & $\dn$ & $zeroable(r_1) \vee zeroable(r_2)$ \\ |
|
221 %$zeroable (r^*)$ & $\dn$ & \textit{false}\\ |
|
222 %\end{tabular} |
|
223 %\end{center}} |
|
224 |
|
225 %\begin{center} |
|
226 %\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$} |
|
227 %\end{center} |
|
228 |
|
229 %\end{frame} |
|
230 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
231 |
|
232 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
233 \begin{frame}[c] |
|
234 \frametitle{Correctness of the Matcher} |
|
235 |
|
236 \begin{itemize} |
|
237 \item We want to prove\medskip |
|
238 \begin{center} |
|
239 \bl{$matches\;r\;s$} if and only if \bl{$s\in L(r)$} |
|
240 \end{center}\bigskip |
|
241 |
|
242 where \bl{$matches\;r\;s \dn nullable(ders\;s\;r)$} |
|
243 \bigskip\pause |
|
244 |
|
245 \item We can do this, if we know\medskip |
|
246 \begin{center} |
|
247 \bl{$L(der\;c\;r) = Der\;c\;(L(r))$} |
|
248 \end{center} |
|
249 \end{itemize} |
|
250 \end{frame} |
|
251 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
252 |
|
253 |
|
254 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
255 \begin{frame}[c] |
|
256 \frametitle{Some Lemmas} |
|
257 |
|
258 \begin{itemize} |
|
259 \item \bl{$Der\;c\;(A\cup B) = |
|
260 (Der\;c\;A)\cup(Der\;c\;B)$}\bigskip |
|
261 \item If \bl{$[] \in A$} then |
|
262 \begin{center} |
|
263 \bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B \;\cup\; (Der\;c\;B)$} |
|
264 \end{center}\bigskip |
|
265 \item If \bl{$[] \not\in A$} then |
|
266 \begin{center} |
|
267 \bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B$} |
|
268 \end{center}\bigskip |
|
269 \item \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$}\\ |
|
270 \small\mbox{}\hfill (interesting case)\\ |
|
271 \end{itemize} |
|
272 |
|
273 \end{frame} |
|
274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
275 |
|
276 |
|
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
278 \begin{frame}[c] |
|
279 \frametitle{Why?} |
|
280 |
|
281 Why does \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$} hold? |
|
282 \bigskip |
|
283 |
|
284 |
|
285 \begin{center} |
|
286 \begin{tabular}{lcl} |
|
287 \bl{$Der\;c\;(A^*)$} & \bl{$=$} & \bl{$Der\;c\;(A^* - \{[]\})$}\medskip\\ |
|
288 & \bl{$=$} & \bl{$Der\;c\;((A - \{[]\})\,@\,A^*)$}\medskip\\ |
|
289 & \bl{$=$} & \bl{$(Der\;c\;(A - \{[]\}))\,@\,A^*$}\medskip\\ |
|
290 & \bl{$=$} & \bl{$(Der\;c\;A)\,@\,A^*$}\medskip\\ |
|
291 \end{tabular} |
|
292 \end{center}\bigskip\bigskip |
|
293 |
|
294 \small |
|
295 using the facts \bl{$Der\;c\;A = Der\;c\;(A - \{[]\})$} and\\ |
|
296 \mbox{}\hfill\bl{$(A - \{[]\}) \,@\, A^* = A^* - \{[]\}$} |
|
297 \end{frame} |
|
298 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
299 |
|
300 |
|
301 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
302 \begin{frame}[c] |
|
303 \frametitle{POSIX Spec} |
|
304 |
|
305 \begin{center} |
|
306 \bl{\infer{[] \in \ONE \to Empty}{}}\hspace{15mm} |
|
307 \bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip |
|
308 |
|
309 \bl{\infer{s \in r_1 + r_2 \to Left(v)} |
|
310 {s \in r_1 \to v}}\hspace{10mm} |
|
311 \bl{\infer{s \in r_1 + r_2 \to Right(v)} |
|
312 {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip |
|
313 |
|
314 \bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)} |
|
315 {\small\begin{array}{l} |
|
316 s_1 \in r_1 \to v_1 \\ |
|
317 s_2 \in r_2 \to v_2 \\ |
|
318 \neg(\exists s_3\,s_4.\; s_3 \not= [] |
|
319 \wedge s_3 @ s_4 = s_2 \wedge |
|
320 s_1 @ s_3 \in L(r_1) \wedge |
|
321 s_4 \in L(r_2)) |
|
322 \end{array}}} |
|
323 |
|
324 \bl{\ldots} |
|
325 \end{center} |
|
326 |
|
327 |
|
328 \end{frame} |
|
329 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
330 |
|
331 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
332 \begin{frame}[t,squeeze] |
|
333 \frametitle{Sulzmann \& Lu Paper} |
|
334 |
|
335 \begin{itemize} |
|
336 \item I have no doubt the algorithm is correct --- |
|
337 the problem is I do not believe their proof. |
|
338 |
|
339 \begin{center} |
|
340 \begin{bubble}[10cm]\small |
|
341 ``How could I miss this? Well, I was rather careless when |
|
342 stating this Lemma :)\smallskip |
|
343 |
|
344 Great example how formal machine checked proofs (and |
|
345 proof assistants) can help to spot flawed reasoning steps.'' |
|
346 \end{bubble} |
|
347 \end{center}\pause |
|
348 |
|
349 %\begin{center} |
|
350 %\begin{bubble}[10cm]\small |
|
351 %``Well, I don't think there's any flaw. The issue is how to |
|
352 %come up with a mechanical proof. In my world mathematical |
|
353 %proof $=$ mechanical proof doesn't necessarily hold.'' |
|
354 %\end{bubble} |
|
355 %\end{center}\pause |
|
356 |
|
357 \end{itemize} |
|
358 |
|
359 \only<3>{% |
|
360 \begin{textblock}{11}(1,4.4) |
|
361 \begin{center} |
|
362 \begin{bubble}[10.9cm]\small\centering |
|
363 \includegraphics[scale=0.37]{msbug.png} |
|
364 \end{bubble} |
|
365 \end{center} |
|
366 \end{textblock}} |
|
367 |
|
368 |
|
369 \end{frame} |
|
370 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
371 |
|
372 \end{document} |
|
373 |
|
374 %%% Local Variables: |
|
375 %%% mode: latex |
|
376 %%% TeX-master: t |
|
377 %%% End: |
|
378 |
|
379 |
|
380 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
38 \begin{frame}[t] |
381 \begin{frame}[t] |
39 \frametitle{2nd CW} |
382 \frametitle{2nd CW} |
40 |
383 |
41 Remember we showed that\\ |
384 Remember we showed that\\ |
42 |
385 |
91 \end{itemize} |
434 \end{itemize} |
92 |
435 |
93 \end{frame} |
436 \end{frame} |
94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
437 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
95 |
438 |
96 |
|
97 |
|
98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
99 \begin{frame}[c] |
|
100 \frametitle{Compilers in Boeings 777} |
|
101 |
|
102 They want to achieve triple redundancy in hardware |
|
103 faults.\bigskip |
|
104 |
|
105 They compile 1 Ada program to |
|
106 |
|
107 \begin{itemize} |
|
108 \item Intel 80486 |
|
109 \item Motorola 68040 (old Macintosh's) |
|
110 \item AMD 29050 (RISC chips used often in laser printers) |
|
111 \end{itemize} |
|
112 |
|
113 \end{frame} |
|
114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
115 |
|
116 |
|
117 |
|
118 |
|
119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
120 \begin{frame}[t] |
|
121 \frametitle{Proofs about Rexps} |
|
122 |
|
123 Remember their inductive definition: |
|
124 |
|
125 \begin{center} |
|
126 \begin{tabular}{@ {}rrl} |
|
127 \bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\ |
|
128 & \bl{$\mid$} & \bl{$\epsilon$} \\ |
|
129 & \bl{$\mid$} & \bl{$c$} \\ |
|
130 & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\ |
|
131 & \bl{$\mid$} & \bl{$r_1 + r_2$} \\ |
|
132 & \bl{$\mid$} & \bl{$r^*$} \\ |
|
133 \end{tabular} |
|
134 \end{center} |
|
135 |
|
136 If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots |
|
137 |
|
138 \end{frame} |
|
139 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
140 |
|
141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
142 \begin{frame}[c] |
|
143 \frametitle{Proofs about Rexp (2)} |
|
144 |
|
145 \begin{itemize} |
|
146 \item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip |
|
147 \item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already |
|
148 holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip |
|
149 \item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already |
|
150 holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip |
|
151 \item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already |
|
152 holds for \bl{$r$}. |
|
153 \end{itemize} |
|
154 |
|
155 \end{frame} |
|
156 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
157 |
|
158 |
|
159 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
160 \begin{frame}[c] |
|
161 |
|
162 \bl{\begin{center} |
|
163 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} |
|
164 $zeroable(\varnothing)$ & $\dn$ & \textit{true}\\ |
|
165 $zeroable(\epsilon)$ & $\dn$ & \textit{false}\\ |
|
166 $zeroable (c)$ & $\dn$ & \textit{false}\\ |
|
167 $zeroable (r_1 + r_2)$ & $\dn$ & $zeroable(r_1) \wedge zeroable(r_2)$ \\ |
|
168 $zeroable (r_1 \cdot r_2)$ & $\dn$ & $zeroable(r_1) \vee zeroable(r_2)$ \\ |
|
169 $zeroable (r^*)$ & $\dn$ & \textit{false}\\ |
|
170 \end{tabular} |
|
171 \end{center}} |
|
172 |
|
173 \begin{center} |
|
174 \bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$} |
|
175 \end{center} |
|
176 |
|
177 \end{frame} |
|
178 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
179 |
|
180 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
181 \begin{frame}[c] |
|
182 \frametitle{Correctness of the Matcher} |
|
183 |
|
184 \begin{itemize} |
|
185 \item We want to prove\medskip |
|
186 \begin{center} |
|
187 \bl{$matches\;r\;s$} if and only if \bl{$s\in L(r)$} |
|
188 \end{center}\bigskip |
|
189 |
|
190 where \bl{$matches\;r\;s \dn nullable(ders\;s\;r)$} |
|
191 \bigskip\pause |
|
192 |
|
193 \item We can do this, if we know\medskip |
|
194 \begin{center} |
|
195 \bl{$L(der\;c\;r) = Der\;c\;(L(r))$} |
|
196 \end{center} |
|
197 \end{itemize} |
|
198 \end{frame} |
|
199 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
200 |
|
201 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
439 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
202 \begin{frame}[c] |
440 \begin{frame}[c] |
203 \frametitle{Induction over Strings} |
441 \frametitle{Induction over Strings} |
204 |
442 |
205 \begin{itemize} |
443 \begin{itemize} |