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