| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Wed, 04 Nov 2020 17:34:52 +0000 | |
| changeset 799 | c18b991eaad2 | 
| parent 538 | e03107e79d26 | 
| permissions | -rw-r--r-- | 
| 
65
 
ade6af51402c
tuned
 
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
 
ade6af51402c
tuned
 
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
 
49c0beef79a1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
76 
diff
changeset
 | 
35  | 
|
| 
312
 
5cdb4d40eb80
update
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
310 
diff
changeset
 | 
36  | 
% beamer stuff  | 
| 459 | 37  | 
\renewcommand{\slidecaption}{CFL 09, King's College London}
 | 
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
38  | 
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
 | 
| 
 
ade6af51402c
tuned
 
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
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
41  | 
\begin{document}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
42  | 
|
| 
 
ade6af51402c
tuned
 
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
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
45  | 
\frametitle{%
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
46  | 
  \begin{tabular}{@ {}c@ {}}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
47  | 
\\[-3mm]  | 
| 459 | 48  | 
\LARGE Compilers and \\[-2mm]  | 
| 537 | 49  | 
\LARGE Formal Languages (8)\\[3mm]  | 
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
50  | 
  \end{tabular}}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
51  | 
|
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
52  | 
\normalsize  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
53  | 
  \begin{center}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
54  | 
  \begin{tabular}{ll}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
55  | 
Email: & christian.urban at kcl.ac.uk\\  | 
| 500 | 56  | 
Office: & N7.07 (North Wing, Bush House)\\  | 
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
57  | 
Slides: & KEATS (also home work is there)\\  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
58  | 
  \end{tabular}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
59  | 
  \end{center}
 | 
| 
 
ade6af51402c
tuned
 
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
 
49c0beef79a1
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
76 
diff
changeset
 | 
62  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
63  | 
|
| 
 
ade6af51402c
tuned
 
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
 
5cdb4d40eb80
update
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
684  | 
|
| 
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
685  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
714  | 
|
| 
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
85b961f1eee9
added
 
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
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
760  | 
\end{document}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
761  | 
|
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
762  | 
%%% Local Variables:  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
763  | 
%%% mode: latex  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
764  | 
%%% TeX-master: t  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
765  | 
%%% End:  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
766  |