slides/slides09.tex-bak
author Christian Urban <christian.urban@kcl.ac.uk>
Wed, 20 Oct 2021 00:06:58 +0100
changeset 847 da2320360f12
parent 538 17acdd516ccd
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
\documentclass[dvipsnames,14pt,t]{beamer}
309
640e4a05cd9b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     2
\usepackage{../slides}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
     3
\usepackage{../langs}
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
     4
\usepackage{../data}
309
640e4a05cd9b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     5
\usepackage{../graphics}
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
     6
\usepackage{../grammar}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
     7
\usepackage{soul}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
     8
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
     9
\tikzset{onslide/.code args={<#1>#2}{%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    10
  \only<#1>{\pgfkeysalso{#2}} % \pgfkeysalso doesn't change the path
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    11
}}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    12
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    13
\makeatletter
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    14
\newenvironment<>{btHighlight}[1][]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    15
{\begin{onlyenv}#2\begingroup\tikzset{bt@Highlight@par/.style={#1}}\begin{lrbox}{\@tempboxa}}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    16
{\end{lrbox}\bt@HL@box[bt@Highlight@par]{\@tempboxa}\endgroup\end{onlyenv}}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    17
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    18
\newcommand<>\btHL[1][]{%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    19
  \only#2{\begin{btHighlight}[#1]\bgroup\aftergroup\bt@HL@endenv}%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    20
}
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
    21
\def\bt@HL@endenv{%b jm 
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    22
  \end{btHighlight}%   
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    23
  \egroup
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    24
}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    25
\newcommand{\bt@HL@box}[2][]{%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    26
  \tikz[#1]{%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    27
    \pgfpathrectangle{\pgfpoint{1pt}{0pt}}{\pgfpoint{\wd #2}{\ht #2}}%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    28
    \pgfusepath{use as bounding box}%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    29
    \node[anchor=base west, fill=orange!30,outer sep=0pt,inner xsep=1pt, inner ysep=0pt, rounded corners=3pt, minimum height=\ht\strutbox+1pt,#1]{\raisebox{1pt}{\strut}\strut\usebox{#2}};
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    30
  }%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    31
}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    32
\makeatother
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
    34
\lstset{morekeywords={def,if,then,else,write,read},keywordstyle=\color{codepurple}\bfseries}
77
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 76
diff changeset
    35
312
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 310
diff changeset
    36
% beamer stuff
459
780486571e38 updated
Christian Urban <urbanc@in.tum.de>
parents: 384
diff changeset
    37
\renewcommand{\slidecaption}{CFL 09, King's College London}
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    40
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
\begin{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
309
640e4a05cd9b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    44
\begin{frame}[t]
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
\frametitle{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
  \begin{tabular}{@ {}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
  \\[-3mm]
459
780486571e38 updated
Christian Urban <urbanc@in.tum.de>
parents: 384
diff changeset
    48
  \LARGE Compilers and \\[-2mm] 
537
feb8a2a42625 updated
Christian Urban <urbanc@in.tum.de>
parents: 500
diff changeset
    49
  \LARGE Formal Languages (8)\\[3mm] 
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
  \end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
  \normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
  \begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
  \begin{tabular}{ll}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
  Email:  & christian.urban at kcl.ac.uk\\
500
c502933be072 updated
Christian Urban <urbanc@in.tum.de>
parents: 459
diff changeset
    56
  Office: & N7.07 (North Wing, Bush House)\\
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
  Slides: & KEATS (also home work is there)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
  \end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
  \end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
309
640e4a05cd9b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    61
\end{frame}
77
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 76
diff changeset
    62
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    63
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    65
\begin{frame}[t,fragile]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    66
\frametitle{Compiling AExps}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    67
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    68
For example \bl{$1 + ((2 * 3) + (4 - 3))$}:\medskip
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    69
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    70
\begin{columns}[T]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    71
\begin{column}{.3\textwidth}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    72
\begin{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    73
\bl{\begin{tikzpicture}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    74
\tikzset{level distance=12mm,sibling distance=4mm}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    75
\tikzset{edge from parent/.style={draw,very thick}}
\Tree [.$+$ [.$1$ ] [.$+$ [.$*$ $2$ $3$ ] [.$-$ $4$ $3$ ]]]
\end{tikzpicture}}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    76
\end{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    77
\end{column}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    78
\begin{column}{.3\textwidth}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    79
\begin{lstlisting}[language=JVMIS,numbers=none]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    80
ldc 1 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    81
ldc 2 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    82
ldc 3 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    83
imul 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    84
ldc 4 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    85
ldc 3 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    86
isub 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    87
iadd 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    88
iadd
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    89
\end{lstlisting}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    90
\end{column}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    91
\end{columns}\bigskip
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    92
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    93
\small
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    94
Traverse tree in post-order \bl{$\Rightarrow$} code for 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    95
stack-machine
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    96
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    97
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
    99
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   100
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   101
\begin{frame}[c,fragile]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   102
\frametitle{Compiling AExps}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   103
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   104
\bl{
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   105
\begin{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   106
\begin{tabular}{lcl}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   107
$\textit{compile}(n, E)$ & $\dn$ & $\pcode{ldc}\;n$\smallskip\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   108
$\textit{compile}(a_1 + a_2, E)$ & $\dn$ \\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   109
\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\;\textit{compile}(a_2, E)\;@\; \pcode{iadd}$}\smallskip\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   110
$\textit{compile}(a_1 - a_2, E)$ & $\dn$ \\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   111
\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{isub}$}\smallskip\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   112
$\textit{compile}(a_1 * a_2, E)$ & $\dn$ \\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   113
\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{imul}$}\smallskip\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   114
$\textit{compile}(a_1 \backslash a_2, E)$ & $\dn$\\ 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   115
\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{idiv}$}\smallskip\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   116
$\textit{compile}(x, E)$ & $\dn$ & $\pcode{iload}\;E(x)$\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   117
\end{tabular}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   118
\end{center}}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   119
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   120
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   121
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   122
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   123
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   124
\begin{frame}[c,fragile]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   125
\frametitle{Compiling Ifs}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   126
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   127
For example
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   128
384
4629448c1bd9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 383
diff changeset
   129
\begin{lstlisting}[mathescape,numbers=none,language=While]
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   130
if 1 = 1 then x := 2 else y := 3
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   131
\end{lstlisting}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   132
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   133
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   134
\begin{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   135
\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   136
   ldc 1
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   137
   ldc 1
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   138
   if_icmpne L_ifelse $\quad\tikz[remember picture] \node (C) {\mbox{}};$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   139
   ldc 2
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   140
   istore 0
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   141
   goto L_ifend $\quad\tikz[remember picture] \node (A) {\mbox{}};$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   142
L_ifelse: $\quad\tikz[remember picture] \node[] (D) {\mbox{}};$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   143
   ldc 3
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   144
   istore 1
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   145
L_ifend: $\quad\tikz[remember picture] \node[] (B) {\mbox{}};$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   146
\end{lstlisting}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   147
\end{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   148
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   149
\begin{tikzpicture}[remember picture,overlay]
  \draw[->,very thick] (A) edge [->,to path={-- ++(10mm,0mm) 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   150
           -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (B.east);
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   151
  \draw[->,very thick] (C) edge [->,to path={-- ++(10mm,0mm) 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   152
           -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (D.east);
\end{tikzpicture}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   153
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   154
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   155
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   156
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   157
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   158
\begin{frame}[c,fragile]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   159
\frametitle{Compiling Whiles}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   160
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   161
For example
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   162
384
4629448c1bd9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 383
diff changeset
   163
\begin{lstlisting}[mathescape,numbers=none,language=While]
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   164
while x <= 10 do x := x + 1
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   165
\end{lstlisting}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   166
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   167
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   168
\begin{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   169
\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   170
L_wbegin: $\quad\tikz[remember picture] \node[] (LB) {\mbox{}};$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   171
   iload 0
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   172
   ldc 10
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   173
   if_icmpgt L_wend $\quad\tikz[remember picture] \node (LC) {\mbox{}};$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   174
   iload 0
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   175
   ldc 1
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   176
   iadd
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   177
   istore 0
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   178
   goto L_wbegin $\quad\tikz[remember picture] \node (LA) {\mbox{}};$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   179
L_wend: $\quad\tikz[remember picture] \node[] (LD) {\mbox{}};$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   180
\end{lstlisting}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   181
\end{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   182
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   183
\begin{tikzpicture}[remember picture,overlay]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   184
  \draw[->,very thick] (LA) edge [->,to path={-- ++(12mm,0mm) 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   185
           -- ++(0mm,17.3mm) |- (\tikztotarget)},line width=1mm] (LB.east);
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   186
  \draw[->,very thick] (LC) edge [->,to path={-- ++(12mm,0mm) 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   187
           -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (LD.east);
\end{tikzpicture}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   188
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   189
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   190
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   191
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   192
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   193
\begin{frame}[c,fragile]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   194
\frametitle{Compiling Writes}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   195
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   196
\small
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   197
\begin{lstlisting}[language=JVMIS,mathescape,
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   198
                   numbers=none,xleftmargin=-6mm]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   199
.method public static write(I)V 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   200
  .limit locals 1 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   201
  .limit stack 2 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   202
  getstatic java/lang/System/out 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   203
                            Ljava/io/PrintStream; 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   204
  iload 0
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   205
  invokevirtual java/io/PrintStream/println(I)V 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   206
  return 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   207
.end method
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   208
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   209
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   210
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   211
iload $E(x)$ 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   212
invokestatic XXX/XXX/write(I)V
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   213
\end{lstlisting}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   214
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   215
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   216
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   217
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   218
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   219
\begin{frame}[c,fragile]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   220
\frametitle{Compiling Main}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   221
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   222
\footnotesize
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   223
\begin{lstlisting}[language=JVMIS,mathescape,
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   224
                   numbers=none,xleftmargin=-6mm]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   225
.class public XXX.XXX
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   226
.super java/lang/Object
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   227
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   228
.method public <init>()V
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   229
    aload_0
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   230
    invokenonvirtual java/lang/Object/<init>()V
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   231
    return
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   232
.end method
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   233
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   234
.method public static main([Ljava/lang/String;)V
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   235
    .limit locals 200
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   236
    .limit stack 200
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   237
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   238
      $\textit{\ldots{}here comes the compiled code\ldots}$
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   239
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   240
    return
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   241
.end method
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   242
\end{lstlisting}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   243
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   244
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   245
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   246
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   247
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   248
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   249
\begin{frame}[c,fragile]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   250
\frametitle{Functional Programming}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   251
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   252
\footnotesize
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   253
\begin{textblock}{13}(0.9,3)
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   254
\begin{lstlisting}[]numbers=none]
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   255
def fib(n) = if n == 0 then 0 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   256
             else if n == 1 then 1 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   257
             else fib(n - 1) + fib(n - 2);
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   258
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   259
def fact(n) = if n == 0 then 1 else n * fact(n - 1);
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   260
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   261
def ack(m, n) = if m == 0 then n + 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   262
                else if n == 0 then ack(m - 1, 1)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   263
                else ack(m - 1, ack(m, n - 1));
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   264
                
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   265
def gcd(a, b) = if b == 0 then a else gcd(b, a % b);                
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   266
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   267
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   268
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   269
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   270
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   271
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   272
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   273
\begin{frame}[c]
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   274
\frametitle{Fun Grammar}
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   275
\bl{
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   276
\begin{plstx}[rhs style=]
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   277
: \meta{Exp} ::= \meta{Var} | \meta{Num}{\hspace{3cm}}
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   278
             |   \meta{Exp} + \meta{Exp} | ... | (\meta{Exp})
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   279
             |   \code{if} \meta{BExp} \code{then} \meta{Exp} \code{else} \meta{Exp}
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   280
             |   \code{write} \meta{Exp} {\hspace{3cm}}
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   281
             |   \meta{Exp} ; \meta{Exp}
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   282
             |   \textit{FunName} (\meta{Exp}, ... , \meta{Exp})\\
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   283
: \meta{BExp} ::= ...\\
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   284
: \meta{Decl} ::= \meta{Def} ; \meta{Decl}
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   285
             | \meta{Exp}\\
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   286
: \meta{Def} ::= \code{def} \textit{FunName} ($\hspace{0.4mm}x_1$, ... , $x_n$) = \meta{Exp}\\               
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   287
\end{plstx}}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   288
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   289
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   290
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
   291
\end{frame}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   292
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   293
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   294
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   295
\begin{frame}[c, fragile]
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   296
\frametitle{Abstract Syntax Trees}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   297
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   298
\footnotesize
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   299
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-1mm]
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   300
abstract class Exp
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   301
abstract class BExp 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   302
abstract class Decl
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   303
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   304
case class Var(s: String) extends Exp
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   305
case class Num(i: Int) extends Exp
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   306
case class Aop(o: String, a1: Exp, a2: Exp) extends Exp
381
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   307
case class If(a: BExp, e1: Exp, e2: Exp) extends Exp
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   308
case class Write(e: Exp) extends Exp
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   309
case class Sequ(e1: Exp, e2: Exp) extends Exp
381
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   310
case class Call(name: String, args: List[Exp]) extends Exp
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   311
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   312
case class Bop(o: String, a1: Exp, a2: Exp) extends BExp
381
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   313
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   314
case class Def(name: String, 
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   315
               args: List[String], 
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   316
               body: Exp) extends Decl
47eceea734c5 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 380
diff changeset
   317
case class Main(e: Exp) extends Decl
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   318
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   319
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   320
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   321
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   322
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   323
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   324
\begin{frame}[c, fragile]
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   325
\frametitle{Sequences}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   326
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   327
Compiling \texttt{exp1 ; exp2}:\bigskip
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   328
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   329
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   330
\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   331
$\textit{compile}$(exp1)
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   332
pop
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   333
$\textit{compile}$(exp2)
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   334
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   335
  
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   336
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   337
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   338
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   339
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   340
\begin{frame}[c, fragile]
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   341
\frametitle{Write}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   342
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   343
Compiling call to \texttt{write(1+2)}:\bigskip
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   344
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   345
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   346
\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   347
$\textit{compile}$(1+2)
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   348
dup
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   349
invokestatic XXX/XXX/write(I)V
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   350
\end{lstlisting}\bigskip
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   351
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   352
\small
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   353
needs the helper method
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   354
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   355
\footnotesize
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   356
\begin{lstlisting}[language=JVMIS, 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   357
                   xleftmargin=2mm, 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   358
                   numbers=none]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   359
.method public static write(I)V 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   360
   .limit locals 1
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   361
   .limit stack 2
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   362
   getstatic java/lang/System/out Ljava/io/PrintStream; 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   363
   iload 0 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   364
   invokevirtual java/io/PrintStream/println(I)V 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   365
   return 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   366
.end method
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   367
\end{lstlisting}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   368
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   369
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   370
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   371
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   372
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   373
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   374
\begin{frame}[t, fragile]
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   375
\frametitle{Function Definitions}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   376
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   377
\footnotesize
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   378
\begin{lstlisting}[language=JVMIS, 
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   379
                   xleftmargin=2mm, 
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   380
                   numbers=none]
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   381
.method public static write(I)V 
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   382
   .limit locals 1
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   383
   .limit stack 2
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   384
   getstatic java/lang/System/out Ljava/io/PrintStream; 
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   385
   iload 0 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   386
   invokevirtual java/io/PrintStream/println(I)V 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   387
   return 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   388
.end method
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   389
\end{lstlisting}\bigskip
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   390
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   391
\small We will need for definitions, like\footnotesize\medskip
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   392
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   393
\begin{lstlisting}[language=JVMIS, 
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   394
                   xleftmargin=2mm, 
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   395
                   numbers=none]
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   396
def fname (x1, ... , xn) = ...                   
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   397
                   
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   398
.method public static fname (I...I)I
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   399
  .limit locals ??
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   400
  .limit stack ?? 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   401
  ??
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   402
.end method
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   403
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   404
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   405
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   406
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   407
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   408
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   409
\begin{frame}[c, fragile]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   410
\frametitle{Stack Estimation}
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   411
\small
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   412
\mbox{}\\[-15mm]
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   413
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   414
\bl{\begin{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   415
\begin{tabular}{@{\hspace{-4mm}}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   416
$\textit{estimate}(n)$ & $\dn$ & $1$\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   417
$\textit{estimate}(x)$ & $\dn$ & $1$\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   418
$\textit{estimate}(a_1\;aop\;a_2)$ & $\dn$ &
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   419
$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   420
$\textit{estimate}(\pcode{if}\;b\;\pcode{then}\;e_1\;\pcode{else}\;e_2)$ & $\dn$ & 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   421
$\textit{estimate}(b) +$\\ 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   422
& & $\quad max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   423
$\textit{estimate}(\pcode{write}(e))$ & $\dn$ & 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   424
$\textit{estimate}(e) + 1$\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   425
$\textit{estimate}(e_1 ; e_2)$ & $\dn$ & 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   426
$max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   427
$\textit{estimate}(f(e_1, ..., e_n))$ & $\dn$ & 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   428
$\sum_{i = 1..n}\;estimate(e_i)$\medskip\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   429
$\textit{estimate}(a_1\;bop\;a_2)$ & $\dn$ &
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   430
$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   431
\end{tabular}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   432
\end{center}}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   433
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   434
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   435
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   436
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   437
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   438
\begin{frame}[fragile]
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   439
\frametitle{Successor Function}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   440
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   441
\begin{textblock}{7}(1,2.5)\footnotesize
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   442
\begin{minipage}{6cm}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   443
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   444
.method public static suc(I)I 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   445
.limit locals 1
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   446
.limit stack 2
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   447
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   448
  ldc 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   449
  iadd
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   450
  ireturn
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   451
.end method 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   452
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   453
\end{minipage}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   454
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   455
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   456
\begin{textblock}{7}(6,8)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   457
\begin{bubble}[5cm]\small
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   458
\begin{lstlisting}[language=Lisp,
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   459
                   basicstyle=\ttfamily, 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   460
                   numbers=none,
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   461
                   xleftmargin=1mm]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   462
def suc(x) = x + 1;
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   463
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   464
\end{bubble}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   465
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   466
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   467
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   468
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   469
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   470
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   471
\begin{frame}[fragile]
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   472
\frametitle{Addition Function}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   473
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   474
\begin{textblock}{7}(1,1.9)\footnotesize
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   475
\begin{minipage}{6cm}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   476
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   477
.method public static add(II)I 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   478
.limit locals 2
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   479
.limit stack 5
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   480
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   481
  ldc 0
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   482
  if_icmpne If_else
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   483
  iload 1
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   484
  goto If_end
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   485
If_else:
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   486
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   487
  ldc 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   488
  isub
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   489
  iload 1
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   490
  invokestatic XXX/XXX/add(II)I
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   491
  invokestatic XXX/XXX/suc(I)I
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   492
If_end:
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   493
  ireturn
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   494
.end method
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   495
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   496
\end{minipage}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   497
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   498
380
1e88390e81aa updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 379
diff changeset
   499
\begin{textblock}{7}(6,6.6)
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   500
\begin{bubble}[7cm]\small
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   501
\begin{lstlisting}[language=Lisp,
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   502
                   basicstyle=\ttfamily, 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   503
                   numbers=none,
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   504
                   xleftmargin=1mm]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   505
def add(x, y) = 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   506
    if x == 0 then y 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   507
    else suc(add(x - 1, y));
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   508
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   509
\end{bubble}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   510
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   511
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   512
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   513
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   514
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   515
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   516
\begin{frame}[fragile]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   517
\frametitle{Factorial}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   518
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   519
\begin{textblock}{7}(1,1.5)\footnotesize
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   520
\begin{minipage}{6cm}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   521
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   522
.method public static facT(II)I 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   523
.limit locals 2
312
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 310
diff changeset
   524
.limit stack 6
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   525
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   526
  ldc 0	
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   527
  if_icmpne If_else_2
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   528
  iload 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   529
  goto If_end_3
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   530
If_else_2:
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   531
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   532
  ldc 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   533
  isub
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   534
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   535
  iload 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   536
  imul
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   537
  invokestatic fact/fact/facT(II)I
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   538
If_end_3:
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   539
  ireturn
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   540
.end method 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   541
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   542
\end{minipage}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   543
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   544
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   545
\begin{textblock}{7}(6,7)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   546
\begin{bubble}[7cm]\small
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   547
\begin{lstlisting}[language=Lisp,
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   548
                   basicstyle=\ttfamily, 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   549
                   numbers=none,
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   550
                   xleftmargin=1mm]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   551
def facT(n, acc) = 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   552
  if n == 0 then acc 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   553
  else facT(n - 1, n * acc);
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   554
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   555
\end{bubble}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   556
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   557
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   558
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   559
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   560
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   561
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   562
\begin{frame}[fragile]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   563
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   564
\begin{textblock}{7}(1,-0.2)\footnotesize
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   565
\begin{minipage}{6cm}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   566
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none, escapeinside={(*@}{@*)}]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   567
.method public static facT(II)I 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   568
.limit locals 2
384
4629448c1bd9 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 383
diff changeset
   569
.limit stack 6
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   570
(*@\hl{facT\_Start:} @*)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   571
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   572
  ldc 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   573
  if_icmpne If_else_2
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   574
  iload 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   575
  goto If_end_3
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   576
If_else_2:
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   577
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   578
  ldc 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   579
  isub
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   580
  iload 0
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   581
  iload 1
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   582
  imul
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   583
  (*@\hl{istore 1} @*)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   584
  (*@\hl{istore 0} @*)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   585
  (*@\hl{goto facT\_Start} @*)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   586
If_end_3:
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   587
  ireturn
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   588
.end method 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   589
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   590
\end{minipage}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   591
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   592
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   593
\begin{textblock}{7}(6,7)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   594
\begin{bubble}[7cm]\small
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   595
\begin{lstlisting}[language=Lisp,
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   596
                   basicstyle=\ttfamily, 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   597
                   numbers=none,
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   598
                   xleftmargin=1mm]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   599
def facT(n, acc) = 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   600
  if n == 0 then acc 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   601
  else facT(n - 1, n * acc);
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   602
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   603
\end{bubble}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   604
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   605
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   606
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   607
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   608
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   609
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   610
\begin{frame}[c, fragile]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   611
\frametitle{Tail Recursion}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   612
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   613
A call to \texttt{f(args)} is usually compiled as\medskip
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   614
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   615
{\small\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   616
  args onto stack
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   617
  invokestatic  .../f 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   618
\end{lstlisting}}\pause
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   619
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   620
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   621
A call is in tail position provided:\medskip
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   622
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   623
{\small\begin{itemize}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   624
\item \texttt{if Bexp then \hl{Exp} else \hl{Exp}}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   625
\item \texttt{Exp ; \hl{Exp}}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   626
\item \texttt{Exp  op Exp}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   627
\end{itemize}}\medskip
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   628
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   629
then a call \texttt{f(args)} can be compiled as\medskip\small
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   630
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   631
\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   632
  prepare environment
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   633
  jump to start of function
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   634
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   635
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   636
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   637
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   638
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   639
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   640
\begin{frame}[c, fragile]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   641
\frametitle{Tail Recursive Call}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   642
\footnotesize
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   643
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   644
\begin{textblock}{13}(-0.3,2)
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   645
\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   646
def compile_expT(a: Exp, env: Mem, name: String): Instrs = 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   647
  ...
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   648
  case Call(n, args) => if (name == n) 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   649
  { 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   650
    val stores = args.zipWithIndex.map 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   651
       { case (x, y) => "istore " + y.toString + "\n" } 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   652
    args.flatMap(a => compile_expT(a, env, "")) ++
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   653
    stores.reverse ++ 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   654
    List ("goto " + n + "_Start\n") 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   655
  } 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   656
  else 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   657
  {
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   658
    val is = "I" * args.length
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   659
    args.flatMap(a => compile_expT(a, env, "")) ++
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   660
    List ("invokestatic XXX/XXX/" + n + "(" + is + ")I\n")
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   661
  }
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   662
\end{lstlisting}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   663
\end{textblock}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   664
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   665
\end{frame}
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   666
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   667
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   668
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   669
  \begin{frame}[c]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   670
  \frametitle{Dijkstra on Testing}
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   671
  
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   672
  \begin{bubble}[10cm]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   673
  ``Program testing can be a very effective way to show the
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   674
  presence of bugs, but it is hopelessly inadequate for showing
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   675
  their absence.''
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   676
  \end{bubble}\bigskip
207
f824e1331fc6 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 206
diff changeset
   677
  
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   678
  \small
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   679
  What is good about compilers: the either seem to work,
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   680
  or go horribly wrong (most of the time).
207
f824e1331fc6 added slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 206
diff changeset
   681
  
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   682
  \end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   683
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   684
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   685
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   686
\begin{frame}[c]
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   687
\frametitle{\Large Proving Programs to be Correct}
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   688
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   689
\begin{bubble}[10cm]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   690
\small
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   691
{\bf Theorem:} There are infinitely many prime 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   692
numbers.\medskip\\
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   693
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   694
{\bf Proof} \ldots\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   695
\end{bubble}\bigskip
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   696
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   697
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   698
similarly\bigskip
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   699
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   700
\begin{bubble}[10cm]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   701
\small
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   702
{\bf Theorem:} The program is doing what 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   703
it is supposed to be doing.\medskip
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   704
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   705
{\bf Long, long proof} \ldots\\
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   706
\end{bubble}\bigskip\medskip
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   707
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   708
\small This can be a gigantic proof. The only hope is to have
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   709
help from the computer. `Program' is here to be understood to be
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   710
quite general (compiler, OS, \ldots).
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   711
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   712
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   713
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   714
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   715
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   716
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   717
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   718
\begin{frame}[c]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   719
\frametitle{Can This Be Done?}
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   720
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   721
\begin{itemize}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   722
\item in 2008, verification of a small C-compiler
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   723
\begin{itemize}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   724
\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   725
\item is as good as \texttt{gcc -O1}, but much, much less buggy 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   726
\end{itemize}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   727
\end{itemize}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   728
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   729
\begin{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   730
  \includegraphics[scale=0.12]{../pics/compcert.png}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   731
\end{center}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   732
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   733
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   734
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   735
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   736
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   737
\begin{frame}[c]
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   738
\frametitle{Fuzzy Testing C-Compilers}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   739
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   740
\begin{itemize}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   741
\item tested GCC, LLVM and others by randomly generating 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   742
C-programs
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   743
\item found more than 300 bugs in GCC and also
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   744
many in LLVM (some of them highest-level critical)\bigskip
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   745
\item about CompCert:
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   746
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   747
\begin{bubble}[10cm]\small ``The striking thing about our CompCert
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   748
results is that the middle-end bugs we found in all other
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   749
compilers are absent. As of early 2011, the under-development
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   750
version of CompCert is the only compiler we have tested for
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   751
which Csmith cannot find wrong-code errors. This is not for
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   752
lack of trying: we have devoted about six CPU-years to the
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   753
task.'' 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   754
\end{bubble} 
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   755
\end{itemize}
206
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 151
diff changeset
   756
383
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   757
\end{frame}
a6a6bf32fade updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 381
diff changeset
   758
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
82
06c3ec0b452e updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 81
diff changeset
   759
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   760
\end{document}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   761
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   762
%%% Local Variables:  
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   763
%%% mode: latex
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   764
%%% TeX-master: t
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   765
%%% End: 
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   766