% $Id: notes.tex,v 1.17 2003/12/10 17:48:51 cclifton Exp $
% -------------------------------------------------------------

\documentclass[11pt]{article}
\usepackage{outliner}
\usepackage{color} % [[[move to notes.sty]]]

% -------------------------------------------------------------
% Import macros
\input{../../Selfless/pac-macros}

% -------------------------------------------------------------
\input{use-full-page}
\setlength{\parindent}{0in}

% -------------------------------------------------------------
% Configure fonts
\renewcommand{\rmdefault}{ppl}  % use Palantino for normal text
\renewcommand{\sfdefault}{pag}  % use Avant Garde for sans serif
\renewcommand{\ttdefault}{phv}  % use Helvetica for code
\renewcommand{\bfdefault}{b}
% Override pac-macros to use tt instead of sf for code
\renewcommand*{\programFontDeclaration}{\normalfont\ttfamily}


% -------------------------------------------------------------
% outliner package configuration
\OutlinePageBreaks{-1}

\OutlineLevelStart0{\section{#1}}

\OutlineLevelStart1{\subsection{#1}}

\OutlineLevelStart2{\begin{itemize}\item{#1}}
\OutlineLevelCont2{\item{#1}}
\OutlineLevelEnd2{\end{itemize}}

\OutlineLevelStart3{\begin{itemize}\item{#1}}
\OutlineLevelCont3{\item{#1}}
\OutlineLevelEnd3{\end{itemize}}

\OutlineLevelStart4{\begin{itemize}\item{#1}}
\OutlineLevelCont4{\item{#1}}
\OutlineLevelEnd4{\end{itemize}}

\OutlineLevelStart5{\begin{itemize}\item{#1}}
\OutlineLevelCont5{\item{#1}}
\OutlineLevelEnd5{\end{itemize}}

\OutlineLevelStart6{\begin{itemize}\item{#1}}
\OutlineLevelCont6{\item{#1}}
\OutlineLevelEnd6{\end{itemize}}


% -------------------------------------------------------------
% Macros for notes [[[move to notes.sty]]]
\newcommand*{\homework}[1]{\note{\textbf{Homework: }{#1}}}
\newcommand*{\question}[1]{\textbf{Q: }{#1}}
\newcommand*{\answer}[1]{\textbf{A: }{#1}}
\newtheorem{defn}{Defn.}[section]
\newcommand*{\grin}{%
   \setbox0=\hbox{$\smile$}%
   \lower 1pt\hbox{\raise 6pt\hbox to \wd0{\bf\hss ..\hss}\llap{\box0}}%
}
\newcommand*{\noteSpace}[1][1in]{\vspace*{#1}}

% --------------------------------------------------------------------------
% Set the showNotes flag to ``true'' to display the instructor's
% notes, or to false to hide them.  Instructor's notes may be placed
% in a ``notes'' environment, for multiple line notes, as the argument
% of the ``note'' command, for shorter notes, or the ``mathNote''
% command, for mathematical expressions.  The notes environment leaves 
% extra-space in the output, assuming that students will write larger 
% than the font size.  The environment and commands use the
% color package to set the text in white on white.  A consequence is
% that the text may be present in the raw output file, depending on
% the driver used.  [[[move to notes.sty, make showNotes an package 
% local variable controlled by options student/instructor, with the 
% latter as the default]]]
\newboolean{showNotes}
\setboolean{showNotes}{true}%{false}
\newcommand*{\noteFormattingDecl}{\sffamily\color{blue}}
\newcommand*{\internalNoteFormattingDecl}{}
\ifthenelse {\boolean{showNotes}}
	    {\renewcommand*{\internalNoteFormattingDecl}
	      {\noteFormattingDecl}}
	    {\renewcommand*{\internalNoteFormattingDecl}
	      {\noteFormattingDecl\color{white}}}

% notes environment uses a box to calculate the appropriate amount of 
% vertical space to skip
\newsavebox{\notesBox}
\newenvironment{notes}
	       {\begin{lrbox}{\notesBox}%
                   \begin{minipage}[t]{\linewidth}\internalNoteFormattingDecl
	       }
	       {\end{minipage}\end{lrbox}%
		 \usebox{\notesBox}\vspace*{\ht\notesBox}\vspace*{\dp\notesBox}
	       }

\newcommand*{\note}[1]{{\internalNoteFormattingDecl{#1}}}

\newcommand*{\mathNote}[1]{\ensuremath{
    \mbox{\internalNoteFormattingDecl${#1}$}
}}

% -------------------------------------------------------------
% Other macros
\newcommand*{\fn}[2]{(\lambda {#1} . {#2})}
\newcommand*{\app}[2]{({#1} \; {#2})}
\newcommand*{\meaningOf}[2]{{\ldblbrack {#1} \rdblbrack}_{#2}}

% -------------------------------------------------------------
\begin{document}

\title{Course Notes: Operational Semantics and\\
the Parameterized Aspect Calculus}

\author{
  Curtis Clifton and Gary T.~Leavens\\
  Dept.~of Computer Science\\
  Iowa State University\\
  226 Atanasoff Hall\\
  Ames, IA 50011-1040 USA\\
  \texttt{\{cclifton,leavens\}@cs.iastate.edu}
}

\maketitle

\begin{Outline}

\Level 0 {Motivation}

\Level 1 {Review \cite{Clifton-Leavens03,Filman-Friedman04}}

\Level 2 {Quantification}
\begin{defn}[Quantified Statements]
  have an effect on many places \emph{in the program}
\end{defn}

\begin{notes}
  as opposed to ``in the underlying code'', which is biased toward
  the base + aspects model
\end{notes}

\Level 2 {Obliviousness}
\begin{defn}[Obliviousness]
  the execution of cross-cutting code $A$
  without any reference to $A$ from the client code that $A$
  cross-cuts
\end{defn}

\Level 3 {\note{semantic} interaction}

\Level 3 {without \note{syntactic} coupling} 

\Level 2 {Modular Reasoning}

Understanding a module $M$ based on:

\Level 3 {\note{the code \emph{in} $M$,}}
\Level 3 {\note{the code \emph{surrounding} $M$, and}}
\Level 3 {\note{the \emph{signature} and \emph{specification} of any modules
  referred to by that code.}}

\Level 2 {Behavioral Subtyping Analogy}

\Level 3 Behavioral subtyping in OOP: 

an overriding method must \note{satisfy the specification of the overridden
method}

\Level 3 Behavioral subtyping is a \emph{discipline}

\Level 4 It places constraints on \note{the subtype programmer}

\Level 4 It provides the benefit of modular reasoning \note{for clients}

\Level 3 What about AOP?

\question{Can a language have quantification and obliviousness
  \emph{and} allow modular reasoning?}

\begin{notes}
It isn't clear.

\question{Is there a discipline like behavioral subtyping that would
  allow modular reasoning in aspect-oriented programming languages?
  in AspectJ?}
\end{notes}

\Level 1 {Spectators and Assistants \cite{Clifton-Leavens02b}}

\Level 2 {Assistants}

\Level 3 can change the behavior of \note{advised code}

\Level 3 must be explicitly accepted by either

\Level 4 the module containing the advised join points,

\note{(all clients see the effects)}

\Level 4 or a client of that module

\note{(only that client sees the effects)}

\Level 2 {Spectators}

\begin{defn}
  A \emph{spectator} is an aspect that \note{``does not change the behavior
  of any other module.''}
\end{defn}

\question{What might that mean?  What is ``spectator-ness''?}

\Level 3 Safety and Liveness \cite{Vaandrager03}

\begin{defn}
  A \emph{safety property} says that \note{nothing bad happens}
\end{defn}

\begin{defn}
  A \emph{liveness property} says that \note{eventually something good
  happens}
\end{defn}

\Level 4 Before-advice that immediately went into an infinite loop
would \note{be \emph{safe} but not \emph{live}}

\Level 4 Before-advice that deleted all the files on your hard drive
and then proceeded to the original method would \note{be \emph{live} but not
\emph{safe}}

\Level 3 Spectators and Safety

Some possible interpretations:

\begin{itemize}
\item A spectator cannot \note{modify any state but its own}

\item A spectator cannot \note{violate the specification of advised modules}
\end{itemize}

\question{Is it that simple?  Are there any problems with these notions?}

\begin{notes}
What about I/O?

Can we modularly find all the advised modules?  What about quantification?
\end{notes}

\Level 3 Spectators and Liveness

Goal: Spectators must always allow the advised method \note{to execute with
its original arguments and must return the result unchanged.}
  
\question{Is this decidable?}

\begin{notes}
  No! by reduction from the halting problem.
\end{notes}
  
What if we:
  
\begin{itemize}
\item Restrict control flow constructs in spectator advice \note{to make the
  problem decidable?}

\begin{notes}
  \question{What constructs could we allow? loops? method calls?
    mathematical expressions?}
\end{notes}
  
\item Run spectators \note{in a separate thread?}

\begin{notes}
  \question{What if advice isn't finished before advised method is
    called again?}
\end{notes}
  
\item \sloppy Approximate by \note{prohibiting spectators from using
  around-advice or throwing checked exceptions?}
\end{itemize}

\Level 2 Do you buy it? \note{[Direct discussion towards needing
formal proof.]}

\Level 3 Which of these notions of ``spectator-ness'' could be
statically enforced?  \note{All but the specification safety property
(and perhaps that could be if the specfications were sufficiently
restricted).}

\Level 3 Do spectators and assistants provide modular reasoning?  How
do we know?

\Level 3 Can we implement reasonable aspect-oriented programs under
these restrictions?

\Level 1 {Why formal semantics?}

\begin{defn}
  A \emph{formal semantics} is a \note{mathematically complete description of
  a programming language}
\end{defn}

\Level 2 {Makes proofs about language properties tractable}

\Level 2 {\emph{Lingua franca} of programming language researchers}

\Level 1 {Why core calculi?}

\begin{defn}
  A \emph{core calculus} is a programming language \note{stripped of all but
  its essential elements}
\end{defn}

\question{What is ``essential''?} \note{Depends on the problem}

A core calculus:

\Level 2 {Eliminates \note{``noise''}}

\Level 2 {Makes construction of \note{complete formal semantics tractable}}

\Level 2 {Can be used to define \note{user-level languages}}

\Level 2 Examples

\Level 3 {$\lambda$ calculus and \note{Haskell}}

\Level 3 {Object calculus and \note{Smalltalk}}

\Level 3 {Parameterized aspect calculus and \note{AspectJ?}}

\Level 0 {Introduction to Formal Semantics}

\Level 1 {Kinds of Formal Semantics}

Example: the semantics of a \code{while} loop

\Level 2 {Denotational \cite{Schmidt94}}

\Level 3 Strength: \note{proving properties about the language}

\Level 3 Map values in language to \note{mathematical entities, like
$\set{\T, \F}$ or the natural numbers}

\Level 3 Model operations in language as \note{mathematical operations, like
$\wedge$, $\neg$, or $+$}

\Level 3 Example:

\[
\meaningOf{\mcode{while }E\mcode{ do }C\mcode{;}}{s} = w(s)
\text{, where }w(s) = \mathit{if}(\meaningOf{E}{s}, w(\meaningOf{C}{s}), s)
\]

\begin{notes}
$s$ is the state, typically a mapping from variables to values

Read double brackets as ``the meaning of foo in the state $s$''.

$w$ is recursive
\end{notes}

$\meaningOf{}{s}$ is overloaded:

\Level 4 {$\meaningOf{E}{s} \ofType \mathit{boolean}$}

\Level 4 {$\meaningOf{C}{s} \ofType \mathit{state}$}

\Level 4 {\question{what is the type of the $\mathit{if}$ function?}}

\note{\answer{
$\mathit{if} \ofType \mathit{Boolean} \times \mathit{State} \times
\mathit{State} \rightarrow \mathit{State}$}}

\Level 2 {Axiomatic \cite{Baumgartner00}}

\Level 3 Strength: \note{proving properties about actual programs}

\Level 3 Map values in language to \note{mathematical entities}

\Level 3 Describe operations using \note{logical assertions, for
example pre- and post-conditions and loop invariants}

\Level 3 Uses \emph{Hoare triples}: $\set{P} C \set{Q}$

\Level 4 {$P$ is a \note{pre-condition}}

\Level 4 {$Q$ is a \note{post-condition}}

\Level 4 {For two states $s$ and $s'$ we write:}

\[
(s,s') \vDash \set{P} C \set{Q} \text{ iff } 
\mathNote{\meaningOf{P}{s} \wedge (\meaningOf{C}{s} = s') 
  \wedge \meaningOf{Q}{s'}}
\]

\begin{notes}
We say ``the Hoare triple $\set{P} C \set{Q}$ is valid for the pair of
states $(s,s')$.''
\end{notes}

\Level 3 Example:

\[
{\inferrule  {
    \mathNote{\set{I \wedge E}} C \set{I}
  }{%-------------------------------------------------------------
    \set{I} \mcode{while $E$ do $C$;} \mathNote{\set{I \wedge \neg E}}
  }
}
\]


$I$ is the \note{loop invariant}

\begin{notes}
Typically the rule used is actually:

\[
{\inferrule  {
    P \implies I\\
    \set{I \wedge E} C \set{I}\\
    (I \wedge \neg E) \implies Q
  }{%-------------------------------------------------------------
    \set{P} \mcode{while $E$ do $C$;} \set{Q}
  }
}
\]
\end{notes}


\Level 2 {Operational}

\Level 3 Strength: \note{clarity, guides implementation, proving
behavioral properties of the language}

\Level 3 Values in language \note{represent themselves (typically)}

\Level 3 Operations are described by \note{\emph{rewrite rules} that
\emph{reduce} a term to a new term, given that a set of premises is
satisfied.}

General form:

\[
{\inferrule {
    \mathit{premise}_1\\
    ...\\
    \mathit{premise}_n
  }{%-------------------------------------------------------------
    \mathit{Env} \vdash a \leadsto b
  }
}
\]

\begin{notes}
$\mathit{Env}$ is an environment

$a$ and $b$ might be terms, or might be sequences describing the state
  of some virtual machine (e.g., term + state)
\end{notes}

\Level 3 Two sorts of operational semantics

\Level 4 Small Step: a sub-term of $a$ is replaced with a new sub-term
to form $b$ \note{rules chain horizontally}

Example:

The semantics of the \code{if} statement is:

\begin{mathpar}
{\inferrule{
    \quad
  }{%-------------------------------------------------------------
    \vdash {\mcode{if true then $C_0$ else $C_1$} \cdot s} \rightarrow
    {C_0 \cdot s}
  }
}

{\inferrule{
    \quad
  }{%-------------------------------------------------------------
    \vdash {\mcode{if false then $C_0$ else $C_1$} \cdot s} \rightarrow
    \mathNote{C_1 \cdot s}
  }
}

{\inferrule{
    \vdash {E \cdot s} \rightarrow {E' \cdot s'}
  }{%-------------------------------------------------------------
    \vdash {\mcode{if $E$ then $C_0$ else $C_1$} \cdot s} \rightarrow
    \mathNote{\mcode{if $E'$ then $C_0$ else $C_1$} \cdot s'}
  }
}
\end{mathpar}

and the semantics of statement sequencing is:

\begin{mathpar}
{\inferrule{
  }{%-------------------------------------------------------------
    \vdash {\mcode{skip; }C_1 \cdot s} \rightarrow {C_1 \cdot s}
  }
}

{\inferrule{
    \mathNote{\vdash {C_0 \cdot s} \rightarrow {C_0' \cdot s'}}
  }{%-------------------------------------------------------------
    \vdash {C_0\mcode{; }C_1 \cdot s} \rightarrow 
    \mathNote{C_0'\mcode{; }C_1 \cdot s'}
  }
}
\end{mathpar}

Using these, the semantics of the \code{while} statement is
\cite{Rugina02}:

\begin{mathpar}
{\inferrule{
    \quad
  }{%-------------------------------------------------------------
    \vdash {\mcode{while $E$ do $C$;} \cdot s} \rightarrow
    { \mcode{if $E$ then }\mathNote{C \mcode{; while }E\mcode{ do }C\mcode{;}}
      \mcode{ else skip} \cdot s}
  }
}
\end{mathpar}

\begin{notes}
  Reduction terminates with $\sequence{\mcode{skip},s}$.
\end{notes}

\Level 4 Big Step (a.k.a. ``natural''): $a$ is reduced to a value in
one (big) step \note{rules stack vertically}

\note{Sometimes when people (e.g., Abadi and Cardelli) say
``operational semantics'', they mean big step}

Example:

\begin{mathpar}
{\inferrule{
    \vdash {E \cdot s} \leadsto {\mcode{false} \cdot s'}
  }{%-------------------------------------------------------------
    \vdash {\mcode{while $E$ do $C$;} \cdot s} \leadsto s'
  }
}

{\inferrule{
    \vdash {E \cdot s} \leadsto {\mcode{true} \cdot s_e}\\
    \vdash {C \cdot s_e} \leadsto s' \\
    \mathNote{\vdash {\mcode{while $E$ do $C$;} \cdot s'} \leadsto s''}
  }{%-------------------------------------------------------------
    \vdash {\mcode{while $E$ do $C$;} \cdot s} \leadsto s''
  }
}
\end{mathpar}

\begin{notes}
The result of reducing a statement is just the state.

Reducing an expression just yields a value, assuming expressions
cannot have side effects.
\end{notes}

\Level 2 Other kinds of formal semantics

\Level 3 Labelled transition systems \note{(enhancement of small step op sem)}

\Level 3 Chemical semantics

\Level 1 {Operational semantics for the $\lambda$ calculus}

\Level 2 {Small step semantics \note{(review, but in Abadi and
Cardelli format)}}

\Level 3 Rules

\Level 4 Top-level, one-step reduction \note{omitting alpha and eta rules}
\begin{mathpar}
{\inferrule[$\beta$]{
    \quad
  }{%-------------------------------------------------------------
    \vdash \app{\fn{x}{e}}{e'} \rightarrowtail e\subst{x}{e'}
  }
}
\end{mathpar}

\note{A\&C substitution style, and sometimes the $x$ is omitted}

\Level 4 One-step reduction

\begin{defn}
  A \emph{context} $\context[C]{\hole}$ is a term with \note{a single hole.}

  $\context[C]{e}$ represents the result of \note{filling the hole with the
  term $e$ (possibly capturing free variables of $e$).}
\end{defn}

\[
{\inferrule{
    \vdash e \rightarrowtail e'\\
    \context[C]{\hole} \text{ is any context}
  }{%-------------------------------------------------------------
    \vdash \context[C]{e} \rightarrow \context[C]{e'}
  }
}
\]

\Level 4 Many-step reduction

$\twoheadrightarrow$ is the \note{reflexive transitive closure of
$\rightarrow$}

\Level 4 Example

\begin{notes}
\begin{mathpar}
{\inferrule*{
    {\inferrule*{
      }{%-------------------------------------------------------------
        \vdash \app{\fn{\mcode{z}}{\mcode{z}}}{2} \rightarrowtail 2
      }
    }\\
    \context[C]{\hole} = \app{\fn{\mcode{y}}{3}}{\hole}
  }{%-------------------------------------------------------------
    \vdash \app{\fn{\mcode{y}}{3}}{\app{\fn{\mcode{z}}{\mcode{z}}}{2}} \rightarrow
    \app{\fn{\mcode{y}}{3}}{2}
  }
}

{\inferrule*{
    {\inferrule*{
      }{%-------------------------------------------------------------
        \vdash \app{\fn{\mcode{y}}{3}}{2} \rightarrowtail 3
      }
    }\\
    \context[C]{\hole} = \hole
  }{%-------------------------------------------------------------
    \vdash \app{\fn{\mcode{y}}{3}}{2} \rightarrow 3
  }
}
\end{mathpar}

Rules chain horizontally
\end{notes}

\Level 3 Non-deterministic:

\begin{notes}
\[
\app{\fn{\mcode{y}}{3}}
    {\app{\fn{\mcode{x}}{\app{\mcode{x}}{\mcode{x}}}}
      {\fn{\mcode{x}}{\app{\mcode{x}}{\mcode{x}}}}}
\]
\end{notes}

Can be made deterministic by restricting the shape of contexts.

\Level 4 Normal order: \note{$\context[C]{\hole} \is \hole \syntaxOr
\app{\context[C]{\hole}}{e}$}

\Level 4 Applicative order?

\begin{notes}
Need a notion of values

$\context[C]{\hole} \is \hole \syntaxOr \app{v}{\context[C]{\hole}}
\syntaxOr \app{\context[C]{\hole}}{e}$

Need to restrict the $\beta$ rule to reduce only terms of the form
$\app{\fn{x}{e}}{v}$.
\end{notes}

\Level 2 {Big step semantics}

\Level 3 Judgment: $\vdash e \leadsto v$

The term $e$ \note{reduces to the value $v$}

\Level 3 Values

\Level 4 {\note{$\lambda$ terms, $\fn{x}{e}$}}

\Level 4 {\note{free variables}}

\Level 3 Rules

\begin{mathpar}
{\inferrule[$\beta$]{
    \mathNote{\vdash e \subst{x}{e'} \leadsto v}
  }{%-------------------------------------------------------------
    \vdash \app{\fn{x}{e}}{e'} \leadsto v
  }
}

{\inferrule[Rator]{
    \mathNote{\vdash e \leadsto v'}\\
    \mathNote{\vdash \app{v'}{e'} \leadsto v}\\
    \mathNote{e \text{ is not a value}}
  }{%-------------------------------------------------------------
    \vdash \app{e}{e'} \leadsto v
  }
}

{\inferrule[Val]{
    \quad
  }{%-------------------------------------------------------------
    \vdash v \leadsto v
  }
}
\end{mathpar}

\question{Do these rules describe applicative order? normal order?
  some other order?} \note{normal order}

\note{[[[The following was done in class.]]]}
\homework{Give the big step semantics for applicative order reduction.
E.C.: implement interpreter based on big step semantics}

\Level 3 Examples
\[
{\inferrule*[right=$\beta$]{
    {\inferrule*[right=Value]{
      }{%-------------------------------------------------------------
        \vdash 3 \leadsto 3
      }
    }
  }{%-------------------------------------------------------------
    \vdash \app{\fn{\mcode{y}}{3}}{\app{\fn{\mcode{z}}{\mcode{z}}}{2}} 
    \leadsto 3
  }
}
\]

\begin{notes}
Let them work out this one:
\[
{\inferrule*[right=Rator]{
    {\inferrule*[right=$\beta$]{
        {\inferrule*[right=Value]{
          }{%-------------------------------------------------------------
            \vdash {\fn{\mcode{y}}{3}} \leadsto {\fn{\mcode{y}}{3}}
          }
        }
      }{%-------------------------------------------------------------
        \vdash {\app{\fn{\mcode{x}}{\mcode{x}}}{\fn{\mcode{y}}{3}}}
        \leadsto {\fn{\mcode{y}}{3}}
      }
    }\\
    {\inferrule*[right=$\beta$]{
        {\inferrule*[right=Value]{
          }{%-------------------------------------------------------------
            \vdash 3 \leadsto 3
          }
        }
      }{%-------------------------------------------------------------
        \vdash \app{\fn{\mcode{y}}{3}}{\app{\fn{\mcode{z}}{\mcode{z}}}{2}} 
        \leadsto 3
      }
    }
  }{%-------------------------------------------------------------
    \vdash 
    \app{\app{\fn{\mcode{x}}{\mcode{x}}}{\fn{\mcode{y}}{3}}}
        {\app{\fn{\mcode{z}}{\mcode{z}}}{2}} 
    \leadsto 3
  }
}
\]
\end{notes}

\Level 3 {\question{Is this semantics deterministic?}}

\note{Yes, because only one rule is applicable to any term.}

\Level 2 {Abadi and Cardelli Proof Style \cite[pp. 79--80]{Abadi-Cardelli96}}

\begin{reduction}
  \begin{premises}
    \begin{premises}
      \judgment[(rule 2)]{Judg_2}
    \end{premises}
    \conclusion[(rule 3)]{Judg_3}
    \begin{premises}
      \judgment[reason]{Judg_4}
    \end{premises}
    \conclusion[(rule 5)]{Judg_5}
  \end{premises}
  \conclusion{Judg_6}
\end{reduction}

Example:

\begin{reduction}
  \begin{premises}
    \begin{premises}
      \judgment[Value]{
        \vdash {\fn{\mcode{y}}{3}} \leadsto {\fn{\mcode{y}}{3}}
      }
    \end{premises}
    \conclusion[$\beta$]{
      \vdash {\app{\fn{\mcode{x}}{\mcode{x}}}{\fn{\mcode{y}}{3}}}
      \leadsto {\fn{\mcode{y}}{3}}
    }
    \begin{premises}
      \judgment[Value]{
        \vdash 3 \leadsto 3
      }
    \end{premises}
    \conclusion[$\beta$]{
      \vdash \app{\fn{\mcode{y}}{3}}{\app{\fn{\mcode{z}}{\mcode{z}}}{2}} 
      \leadsto 3
    }
  \end{premises}
  \conclusion[Rator]{
    \vdash 
    \app{\app{\fn{\mcode{x}}{\mcode{x}}}{\fn{\mcode{y}}{3}}}
        {\app{\fn{\mcode{z}}{\mcode{z}}}{2}} 
        \leadsto 3
  }
\end{reduction}

\Level 1 {Untyped Object Calculus, $\varsigma$}

\Level 2 {Syntax}

\begin{mathpar}
\symbolLineStretch
\begin{array}[t]{p{0.93in}rcl}
\raggedleft variables & x & \in & \Vars \\
\raggedleft labels & l & \in & \Labels \\
\raggedleft terms & a, b, c & \is & x \\
&& \syntaxOr & \object \\
&& \syntaxOr & \invoke{a}{l} \\
&& \syntaxOr & \update{a}{l}{x}{b}
\end{array}
\end{mathpar}

%\Level 2 {Small step semantics}

\Level 2 {Big step semantics \note{(omitting small step semantics due
    to limited time)}}

\homework{Implement a stack object using the object calculus}

\Level 3 {Object\note{: a \emph{set} of pairs of \emph{labels} and
    \emph{methods}}}

\[
{\inferrule[Red Object]{
  }{%-------------------------------------------------------------
    \vdash \object \leadsto \object
  }
}
\]

Example: \code{[pos=\s(x)x.n, n=\s(x)2]}\note{, where \code{2} is
  shorthand for an object that represents the natural number 2.}

\Level 3 {Method Selection\note{: reduces the body of the \emph{named
      method}, substituting object for the \emph{self parameter}}}

\[
{\inferrule[Red Select]{
    \vdash a \leadsto \object \\
    \vdash b_j \subst{x_j}{\object} \leadsto v \\
    j \in I
  }{%-------------------------------------------------------------
    \vdash \invoke{a}{l_j} \leadsto v
  }
}
\]

Example: \code{[pos=\s(x)x.n, n=\s(x)2].pos} 

{
\begin{reduction}
  \begin{premises}
    \judgment[Red Object]{
      \vdash {\objTempOne{\mcode{pos}=\nmethod{\mcode{x}}{\invoke{\mcode{x}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{x}}{\mcode{2}}}}
      \leadsto {\objTempOne{\mcode{pos}=\nmethod{\mcode{x}}{\invoke{\mcode{x}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{x}}{\mcode{2}}}}
    }
    \judgment{\mcode{pos} \in \set{\mcode{pos},\mcode{n}}}
    \begin{premises}
      \judgment[Red Object]{
        \vdash {\objTempOne{\mcode{pos}=\nmethod{\mcode{x}}{\invoke{\mcode{x}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{x}}{\mcode{2}}}}
        \leadsto {\objTempOne{\mcode{pos}=\nmethod{\mcode{x}}{\invoke{\mcode{x}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{x}}{\mcode{2}}}}
      }
      \judgment{\mcode{n} \in \set{\mcode{pos},\mcode{n}}}
      \judgment[Red Object]{
        \vdash {\mcode{2}} \leadsto {\mcode{2}}
      }
    \end{premises}
    \conclusion[Red Select]{
      \vdash {\invoke{\objTempOne{\mcode{pos}=\nmethod{\mcode{x}}{\invoke{\mcode{x}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{x}}{\mcode{2}}}}{\mcode{n}}}
      \leadsto {\mcode{2}}
    }
  \end{premises}
  \conclusion[Red Select]{
    \vdash {\invoke{\objTempOne{\mcode{pos}=\nmethod{\mcode{x}}{\invoke{\mcode{x}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{x}}{\mcode{2}}}}{\mcode{pos}}}
    \leadsto {\mcode{2}}
  }
\end{reduction}
}

\Level 3 {Method update\note{: generates a \emph{new} object, with the
    given method replacing the named method}}

\[
{\inferrule[Red Update]{
    \vdash a \leadsto \object \\
    j \in I
  }{%-------------------------------------------------------------
    \vdash \update{a}{l_j}{x}{b} \leadsto
    \objTempOne{l_j=\s(x)b, \setComp{l_i=\s(x_i)b_i}{i \in I \setminus j}}
  }
}
\]

\question{What's the result of reducing this term: 
  \code{[pos=\s(x)x.n, n=\s(x)2].n \upds \s(x)3}}

\note{\answer{\code{[pos=\s(x)x.n, n=\s(x)3]}}}

\question{What about this one: 
  \code{[pos=\s(x)x.n, n=\s(x)2].pos \upds \s(x)x.n.succ}}

\note{\answer{\code{[pos=\s(x)x.n.succ, n=\s(x)2]}}}

\question{What happens if we select \code{pos} on the result?}

\note{\answer{\code{3}, assuming $\mcode{2.succ} \leadsto \mcode{3}$}}

\Level 2 {Syntactic sugar}

\Level 3 {Fields: methods in which \note{the self parameter does not
appear free}}

\code{[pos=\s(x).n, n=2]} desugars to \note{\code{[pos=\s(x).n, n=\s(y)2]}
where \code{y} is not free in \code{2}}

\code{[pos=\s(x).n, n=2].n \gets\ 3} desugars to
\note{\code{[pos=\s(x).n, n=3]}}

\Level 3 {Lambda expressions}

Can translate untyped $\lambda$ calculus into the $\varsigma$ calculus.

Let $\translate{}$ map $\lambda$ calculus to $\varsigma$ calculus as follows:

\[
\begin{array}{rcl}
\translate{x} & = & x \\
\translate{\app{e_1}{e_2}} & = & 
\invoke{(\invoke{\translate{e_1}}{\mathit{arg}} \gets \translate{e_2})}
       {\mathit{val}} \\
\translate{\fn{x}{e}} & = &
\mathNote{\objTempOne{arg=0, val=\s(s)\translate{e}\subst{x}{s.arg}}}
\end{array}
\]

\homework{Translate some lambda calculus expressions and reduce them
  in the object calculus}

%\Level 2 {A $\varsigma$-calculus interpreter}
%[[[omit due to time constraints?]]]

\Level 0 {Parameterized Aspect Calculus, \pac
  \cite{Clifton-Leavens-Wand03,Clifton-Leavens-Wand03a} }

\Level 1 {Changes vs. the object calculus}

Object calculus plus aspects \note{plus constants}

\Level 2 {Join point abstraction}

\Level 3 Each reduction step triggers \note{a search for advice}

\Level 3 Search uses a four-part abstraction of the reduction step

\Level 4 {\emph{Reduction kind}, $\rk$\note{, one of $\set{\VAL,\ivk,\upd}$}}

\Level 4 {\emph{Evaluation context}, $\ec$\note{, represents the call stack}}

\Level 4 {\emph{Target signature}\note{, represents the ``shape'' of
the target of the operation}}

\Level 5 either the set of labels in the target object, or

\Level 5 the name of a constant

\Level 4 {Invocation or update \emph{message}}

\Level 5 either a label, or

\Level 5 a functional constant

\Level 3 The search semantics is specified by a \note{\emph{point cut
  description language}, or \emph{PCDL}}

\Level 4 PCDL is a parameter to the calculus, various PCDL may be used

\question{How might this be useful?}

\begin{notes}
\answer{can easily experiment with different PCDL}

\answer{can restrict the set of join points that might be matched}
\end{notes}

\question{What problems might this cause?}

\begin{notes}
\answer{might make the semantics more complex}

\answer{possible that complexity is hidden in the PCDL, making the core calculus ``less core''}
\end{notes}

\Level 4 PCDL consists of two parts: 

\Level 5 {\note{Point cut description syntax, \pcl}}

\Level 5 {\note{Advice matching function, \match}}

\Level 2 {Syntax of \pac}

\Level 3 {All object calculus terms}

\Level 3 {Constants}

\begin{mathpar}
\symbolLineStretch
d \in \Consts

f \in \FConsts

\begin{array}[t]{p{0.93in}rcl}
\raggedleft terms & a, b, c & \is & \ldots \\
&& \syntaxOr & d\\
&& \syntaxOr & \invoke{a}{f}
\end{array}
\end{mathpar}

\begin{notes}
Constants are things like natural numbers

Functional constants are operations like successor

The primary reason for introducing constants is to simplify examples,
going forward they may be eliminated--discuss this if time allows
\end{notes}

\Level 3 {Advice}

\begin{mathpar}
\symbolLineStretch
\pcd \in \pcl

\begin{array}[t]{p{0.93in}rcl}
\raggedleft programs & \progVar & \is & \progTerm {a} {\seqComp{\A}{}} \\
\raggedleft advice
  & \A & \is & \advice {\pcd} {\seqComp{y}{}} {b} \\
\end{array}
\end{mathpar}

\begin{notes}
A program consists of a base term (think ``main'') and a sequence of advice

Advice maps a point cut description to a ``naked method'', define naked method
\end{notes}

\Level 3 {Proceeding}

\begin{mathpar}
\symbolLineStretch
\begin{array}[t]{p{1.5in}rcl}
\raggedleft terms & a, b, c & \is & \ldots \\
&& \syntaxOr & \proceedval() \\
&& \syntaxOr & \proceedivk(a) \\
&& \syntaxOr & \proceedupd(a,\nmethod{x}{b}) \\
&& \syntaxOr & \pi\\
\raggedleft proceed closures & \pi & \is &  
  \procClosure{\VAL}{\valThunk{\nmethodListVar}{v}}() \\
&& \syntaxOr &
  \procClosure{\ivk}{\ivkThunk{\nmethodListVar}{\Svar}{k}}(a) \\
&& \syntaxOr &
  \procClosure{\upd}{\updThunk{\nmethodListVar}{k}}(a,\nmethod{x}{b}) \\
\end{array}
\end{mathpar}

\begin{notes}
Advice can contain \code{proceed} terms

\code{proceed} terms are converted to proceed closures during advice lookup

User programs cannot contain proceed closures
\end{notes}

\Level 2 {Semantics}

\Level 3 Changes

\Level 4 Object calculus reduction rules are changed to \note{add
advice lookup}

\Level 4 Rules are added for:

\Level 5 Constants

\Level 5 Object calculus terms to which advice applies

\Level 5 Proceeding

\Level 3 Helper functions

\Level 4 Advice lookup
\note{Give types of these helper functions.}

\input{../../Selfless/defn-advice-for}

\begin{notes}
  Returns a list of naked methods

  Invokes PCDL's $\match$ function for each piece of advice
\end{notes}

\Level 4 Proceed closure
\begin{mathpar}
\input{../../Selfless/defn-closeprime}
\end{mathpar}

\begin{notes}
  Takes proceed terms in advice and converts them to proceed closures,
  squirreling away any information needed for proceeding.

  These are the most interesting definitions, the others just recurse
  to sub-terms.
\end{notes}

\Level 3 Objects and Basic Constants

\begin{mathpar}
\begin{array}[t]{p{0.93in}rcl}
\raggedleft values & v & \is & d \syntaxOr \object \\
\end{array}

{\inferrule [Red Val 0] {
    \wellformed[\M,\ASeq]{\ec} \\
    \adviceForSix[\M] {\VAL} {\ec} 
                 {\sig{v}}
                 {\emptyStr} {\ASeq} 
                  = \emptySeq
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	    {v} 
            {v}
  }
}

{\inferrule [Red Val 1] {
    \wellformed[\M,\ASeq]{ \ec} \\
    \adviceForSix[\M] {\VAL} {\ec} 
                 {\sig{v}} 
                 {\emptyStr} {\ASeq} 
    = {\nmethod{}{b}} \seqCat \nmethodListVar \\
    {\close{\VAL}(b,{\valThunk{\nmethodListVar}{v}})} = b' \\
    \reduces[\M,\ASeq] {\valAdvContext \contextCat \ec}
	     {b'} 
             {v'} 
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	     {v} 
             {v'}
  }
}
\end{mathpar}

\question{What, in plain English, is the meaning of these two rules?}

\noteSpace[2in]  

Things to note:

\Level 4 {subscripts on the turnstile}

\Level 4 {wellformedness premise}

\Level 4 {\ruleName{Red Val 0} correspondence to \ruleName{Red
    Object}}

\Level 4 {advice lookup}

\Level 5 {join point abstraction}

\Level 5 {Required shape of result in \ruleName{Red Val 1}}

\Level 4 {proceed closure, and information stored}

\Level 4 {evaluation context in last premise of \ruleName{Red Val 1}}

\Level 3 Method Selection
\begin{mathpar}
{\inferrule [Red Sel 0 \textnormal{(where $o \triangleq \object$)}] {
    \reduces[\M,\ASeq] {\ec} 
            {a} {o} \\
    l_j \in \setComp{l_i}{i \in I} \\
    {\adviceForSix[\M] {\ivk} {\ec} 
      {\setComp{l_i}{i \in I}} 
      {l_{j}} {\ASeq} 
    }
    = \emptySeq \\
    \reduces[\M,\ASeq] 
	    {\ivkBodyContext {\setComp{l_i}{i \in I}} {l_{j}}  
	      \contextCat {\ec}}
            {b_{j} \subst{x_{j}}{o}} 
            {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	     {\invoke {a} {l_{j}}} 
             {v}
  }
}

{\inferrule [Red Sel 1 \textnormal{(where $o \triangleq \object$)}] {
    \reduces[\M,\ASeq] {\ec}
	    {a} {o} \\
    l_j \in \setComp{l_i}{i \in I} \\
    {\adviceForSix[\M] {\ivk} {\ec} 
      {\setComp{l_i}{i \in I}} 
      {l_{j}} {\ASeq} 
    }
    = {\nmethod {y} {b}} \seqCat \nmethodListVar \\
    \close{\ivk}(b, \ivkThunk{(\nmethodListVar \seqCat \nmethod {x_{j}} {b_{j}})}
		        {\setComp{l_i}{i \in I}} {l_{j}}) = b' \\
    \reduces[\M,\ASeq] {\ivkAdvContext \contextCat {\ec}}
            {b' \subst{y}{o}}
            {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	     {\invoke {a} {l_{j}}} 
             {v}
  }
}
\end{mathpar}

% The following is written way this to keep the questions together
\question{What, in plain English, is the meaning of these two
  rules?}\hfill~\linebreak \question{Where does the final value come
  from?}

\noteSpace[2in]

Things to note:

\Level 4 {correspondence of \ruleName{Red Sel 0} and \ruleName{Red Select}}

\Level 4 join point abstraction

\Level 4 shape of returned advice

\Level 4 information stored in proceed closure

\Level 4 evaluation context \note{differences}

\Level 3 Functional Constant Application

\begin{notes}
$\delta(f,v')$ means ``apply the functional constant $f$ to the value
  $v'$.  $\delta$ is intentionally underspecified, since we don't say
  what the basic and functional constants are.  Suppose $\FConsts =
  \set{\mcode{succ}}$ and $\Consts$ is the natural numbers:
  $\delta(\mcode{succ},\mcode{3}) = \mcode{4}$.
\end{notes}

\begin{mathpar}
{\inferrule [Red FConst 0] {
    \reduces[\M,\ASeq] {\ec} 
            {a} {v'} \\
    {\adviceForSix[\M] {\ivk} {\ec} 
      {\sig{v'}} 
      {f} {\ASeq} 
    }
    = \emptySeq \\
    \reduces[\M,\ASeq] {\ivkBodyContext {\sig{v'}} {f}  \contextCat {\ec}} 
            {\delta(f,v')} {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	    {\invoke {a} {f}} 
            {v}
  }
}

{\inferrule [Red FConst 1] {
    \reduces[\M,\ASeq] {\ec} 
            {a} {v'} \\
    {\adviceForSix[\M] {\ivk} {\ec} 
      {\sig{v'}} 
      {f} {\ASeq} 
    }
    = {\nmethod {y} {b}} \seqCat \nmethodListVar \\
    \close{\ivk}(b,{\ivkThunk{\nmethodListVar} {\sig{v'}} {f}}) = b' \\
    \reduces[\M,\ASeq] {\ivkAdvContext \contextCat {\ec}} 
            {b' \subst{y}{v'}} 
	    {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	    {\invoke {a} {f}} 
            {v}
  }
}
\end{mathpar}

\question{What is the meaning of these two rules?}

\noteSpace[2in]

Things to note:

\Level 4 {\relax\question{Aren't these rules non-deterministic given the selection rules?} \note{Not if $\FConsts \cup \Labels = \emptySet$}}

\Level 4 {\relax\question{How do these rules differ from the selection rules?}}

\begin{notes}
No label presence test

Join point abstraction uses $\mathit{sig}$ function

The 0 rule uses $\delta$ function
\end{notes}

\Level 3 Method Update

\begin{mathpar}
{\inferrule [Red Upd 0 \textnormal{(where $o \triangleq \object$)}] {
    \reduces[\M,\ASeq] {\ec}
            {a} {o} \\
    l_j \in \setComp{l_i}{i \in I} \\
    \adviceForSix[\M] {\upd} {\ec}
                  {\setComp{l_{i}}{i \in I}} 
                  {l_{j}} {\ASeq} 
                  = \emptySeq
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	     {\update {a} {l_{j}} {x} {b}} 
             {\objTempOne{
                 \setComp{l_{i}=\nmethod{x_{i}}{b_{i}}}
                                  {i \in I \setminus \set{j}},
                 l_{j} = \nmethod{x}{b}
               }
             }
  }
}

{\inferrule [Red Upd 1 \textnormal{(where $o \triangleq \object$)}] {
    \reduces[\M,\ASeq] {\ec}
            {a} {o} \\
    \adviceForSix[\M] {\upd} {\ec}
                  {\setComp{l_{i}}{i \in I}} 
                  {l_{j}} {\ASeq}
    = \nmethod{\mathit{targ}, \mathit{rval}}{b'} \seqCat \nmethodListVar\\
    \close{\upd}(b',{\updThunk{\nmethodListVar}{l_{j}}}) = b'' \\
    \reduces[\M,\ASeq] {\updAdvContext \contextCat \ec}
	    {b'' {\capSubst{\mathit{rval}}{b\subst{x}{\mathit{targ}}}
		 {\mathit{targ}}}
              {\subst{\mathit{targ}}{o}}}
	    {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	     {\update {a} {l_{j}} {x} {b}} 
             {v}
  }
}
\end{mathpar}

Things to note:

\Level 4 {Correspondence of \ruleName{Red Upd 0} and \ruleName{Red Update}}

\Level 4 {Evaluation context in \ruleName{Red Upd 1}}

\Level 4 {Data used for proceed closure}

\Level 4 {Shape of returned advice: \emph{two} parameters}

\Level 5 {$\mathit{targ}$, corresponds to \note{the target object,
    $o$, of the update operation.}}

\Level 5 {$\mathit{rval}$, corresponds to \note{the body, $b$, of the
    update's r-value.}}

\Level 4 {\emph{two} kinds of substitution}

\Level 5 {$b \subst{x}{c}$ is normal capture-avoiding substitution}

Key rules: \note{the rest just recurse over the grammar}
\[
\renewcommand*{\arraystretch}{1.25}
\begin{array}{rclr}
  (\nmethod{y}{b}) \subst {x} {c} & \triangleq &
    \multicolumn{2}{l}{\nmethod{y'} (b \subst {y} {y'} \subst {x} {c})}\\
&& \multicolumn{2}{r}{
    \text {where } y' \notin \FV{\nmethod{y}{b}} \cup \FV{c} \cup \set{x}} \\
  x \subst {x} {c} & \triangleq & c \\
  y \subst {x} {c} & \triangleq & y & \text{if } x \not= y \\
\end{array}
\]

\Level 5 {$b'' \capSubst {x}{\mathit{c}}{\mathit{z}}$ says: in $b''$
  replace all \note{free} occurances of $x$ with $c$,
  capturing any \note{free} occurances of $z$ in $c$}

Key rules: \note{varref is same as above, the rest just recurse over
  the grammar}
\[
\renewcommand*{\arraystretch}{1.25}
\begin{array}{rclr}
  (\nmethod{z}{b}) \capSubst{x}{c}{z} & \triangleq &
    \nmethod{z} (\capSubst{x}{c}{z}) & \mathNote{\text{no renaming}}\\
  (\nmethod{y}{b}) \capSubst{x}{c}{z} & \triangleq &
    \nmethod{y'} (b \subst {y} {y'} \capSubst{x}{c}{z}) & 
    \mathNote{\text{renaming}}\\
&&\multicolumn{2}{r}{
    \text{if } y \not= z
    \text {, where } y' \notin \FV{\nmethod{y}{b}} \cup \FV{c} \cup \set{x}} \\
\end{array}
\]

\question{Which of these rules does the capturing?}

\note{\answer{the first}}

\Level 4 {Why two kinds of substitution? \note{solicit ideas}}

\Level 5 {$b \subst{x}{\mathit{targ}}$: \note{renames the self
    parameter in the body, $b$, of the original r-value}}

\Level 5 {$\mathit{targ}$-capturing substitution for $\mathit{rval}$
in the advice body, $b''$, lets advice author:}

capture occurrences of the self-parameter\note{, by placing
$\mathit{rval}$ under a $\s(\mathit{targ})$ binder}

\emph{or}

not capture occurrences of the self-parameter\note{, by not placing
$\mathit{rval}$ under a binder or by placing it under a
non-$\mathit{targ}$ binder}

\Level 4 Examples:

\[
\mcode{[n=\s(y)0, pos=\s(p)p.n].pos \upds\ \s(x)x.n.succ}
\]

\Level 5 {In the absence of advice, this would reduce to:}

\begin{notes}
\[
\mcode{[n=\s(y)0, pos=\s(x)x.n.succ]}
\]
\end{notes}

\question{What happens if we update \code{n} to 2 in this object and then
  select \code{pos}?} 

\note{\answer{We get back 3.}}



\Level 5 {Advice designed to avoid capture: \note{\code{targ} does not appear
  bound in $b''$}}
\[
\mcode{\s(targ,rval)\proceedupd(targ, \s(z)rval)}
\]

\begin{notes}
  fixes the value of the \code{pos} method to the result of evaluating
  the new method body, \code{x.n.succ}, substituting the original
  target object for \code{x}:
\end{notes}

Assuming no other advice:
\[
b'' = \procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}
\mcode{(targ, \s(z)rval)}
\]

\note{Underbars indicate target of next substitution}

\begin{multline*}
\mcode{\procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}(targ, \s(z)rval)}
\capSubst{\mcode{rval}}
         {\underbar{\mcode{x.n.succ}} 
	   \subst{\mcode{x}}{\mcode{targ}}}{\mcode{targ}}\\
\shoveright{\subst{\mcode{targ}}{\mcode{[n=\s(y)0, pos=\s(p)p.n]}}} \\
% -------------------------------------------------------------
\shoveleft{{} = \underbar{\mcode{\procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}(targ, \s(z)rval)}}}
\capSubst{\mcode{rval}}{\mathNote{\mcode{targ.n.succ}}}{\mcode{targ}}\\
\shoveright{\subst{\mcode{targ}}{\mcode{[n=\s(y)0, pos=\s(p)p.n]}}} \\
% -------------------------------------------------------------
\shoveleft{{} = 
  \underbar{\mcode{\procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}(}\mathNote{\mcode{targ, \s(z){targ.n.succ}}})} \subst{\mcode{targ}}{\mcode{[n=\s(y)0, pos=\s(p)p.n]}}} \\
% -------------------------------------------------------------
\shoveleft{{} = 
  \mcode{\procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}([n=\s(y)0, pos=\s(p)p.n], \s(z)[n=\s(y)0, pos=\s(p)p.n].n.succ)}}
\end{multline*}

The last term will reduce to:
\[
\mcode{[n=\s(y)0, pos=\s(z)[n=\s(y)0, pos=\s(p)p.n].n.succ]}
\]

\question{What happens if we update \code{n} to 2 in this object and then
  select \code{pos}?} 

\note{\answer{We get back 1!}}

\Level 5 {Advice designed to capture: \note{because \code{rval}
    appears under a \code{targ} binder}}

\[
\mcode{\s(targ,rval)\proceedupd(targ,\s(targ)rval.succ)}
\]

\begin{notes}
  uses the body of the update's r-value without causing it to be
  reduced
\end{notes}


Assuming no other advice was found in the advice lookup, then after
closing the $\proceedupd$ sub-term, the substitutions for this advice
are:
\begin{multline*}
\mcode{\procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}(targ,\s(targ)rval.succ)
\capSubst{\mcode{rval}}
         {\underbar{\mcode{x.n.succ}} \subst{\mcode{x}}{\mcode{targ}}}
         {\mcode{targ}}}\\
\shoveright{\subst{\mcode{targ}}{\mcode{[n=\s(y)0, pos=\s(p)p.n]}}} \\
% -------------------------------------------------------------
\shoveleft{ {} =
  \underbar{\mcode{\procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}(targ,\s(targ)rval.succ)}}}
\capSubst{\mcode{rval}} {\mcode{targ.n.succ}} {\mcode{targ}}\\
\shoveright{\subst{\mcode{targ}}{\mcode{[n=\s(y)0, pos=\s(p)p.n]}}} \\
% -------------------------------------------------------------
\shoveleft{ {} =
  \underbar{\mcode{\procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}(targ,\s(targ)\mathNote{\mcode{targ.n.succ}}.succ)}}} \mathNote{\text{ capture!}}\\
\shoveright{\subst{\mcode{targ}}{\mcode{[n=\s(y)0, pos=\s(p)p.n]}}} \\
% -------------------------------------------------------------
\shoveleft{ {} =
  \mcode{\procClosure{\upd}{\updThunk{\emptySeq}{\mcode{pos}}}([n=\s(y)0, pos=\s(p)p.n], \s(targ)\mathNote{\qquad\qquad\qquad\mcode{targ}}.n.succ.succ)}} \\
{}
\end{multline*}

\begin{notes}
  The last targ is not free and so isn't replaced.

  (Those last two targ's should really be renamed, but this is
  alpha equivalent.)
\end{notes}

This term will reduce to:
\[
  \mcode{[n=\s(y)0, pos=\s(targ)targ.n.succ.succ]}
\]

\question{What happens if we update \code{n} to 2 in this object and then
  select \code{pos}?} 

\note{\answer{We get back 4!}}

\Level 3 Proceeding

\Level 4 General ideas:

\Level 5 {Two rules for each kind of advice \note{one for proceeding
    to lower precedence advice, one for proceeding to original
    operation}}

\Level 5 {Rules are very similar to the regular operations,
  \emph{except} \ldots}

\Level 5 {No additional advice lookup \note{subsequent advice and
    original operation are taken from the proceed closure}}

\Level 5 {Proceed closure formed \note{lazily}}

\Level 4 Proceeding from Value Advice

\begin{mathpar}
  {\inferrule [Red VPrcd 0] {
    \wellformed[\M,\ASeq]{\ec}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	    {\procClosure{\VAL}{\valThunk{\emptySeq}{v}}()} 
            {v}
  }
}

{\inferrule [Red VPrcd 1] {
    \wellformed[\M,\ASeq]{\ec} \\
    {\close{\VAL}(b,{\valThunk{\nmethodListVar}{v}})} = b' \\
    \reduces[\M,\ASeq] {\valAdvContext \contextCat \ec}
	    {b'} 
            {v'}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	    {\procClosure{\VAL}
	      {\valThunk{(\nmethod{}{b} \seqCat \nmethodListVar)}{v}}()} 
            {v'}
  }
}
\end{mathpar}

\Level 4 Proceeding from Selection Advice

\begin{mathpar}
  {\inferrule [Red SPrcd 0] {
    \reduces[\M,\ASeq] {\ec}
	    {a} 
            {o} \\
    \reduces[\M,\ASeq]
            {\ivkBodyContext{\setComp{l}{}}{l} \contextCat {\ec}}
            {b \subst{y}{o}} 
            {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] 
            {\ec}
	    {\procClosure{\ivk}
	      {\ivkThunk {\nmethod{y}{b}}{\setComp{l}{}}{l}}(a)} 
            {v}
  }
}

{\inferrule [Red SPrcd 1] {
    \reduces[\M,\ASeq] {\ec}
	    {a} 
            {o} \\
    \nmethodListVar \not= \emptySeq \\
    \close{\ivk}(b,{\ivkThunk {\nmethodListVar}{\setComp{l}{}}{l}}) = b' \\
    \reduces[\M,\ASeq]
            {\ivkAdvContext \contextCat {\ec}}
            {b' \subst{y}{o}} 
            {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	    {\procClosure{\ivk}
	      {\ivkThunk {(\nmethod{y}{b} \seqCat \nmethodListVar)}
		{\setComp{l}{}}{l}}
	      (a)} 
            {v}
  }
}
\end{mathpar}

\question{Where does the target object in the 0 rule come from?}

\note{\answer{the proceed closure's argument}}

\question{Where does the method body evaluated in the 0 rule come from?}

\note{\answer{the proceed closure's thunk \emph{not} the target object}}

\Level 4 Proceeding from Application Advice

\begin{mathpar}
{\inferrule [Red FPrcd 0] {
    \reduces[\M,\ASeq] 
            {\ec}
	    {a} 
            {v'} \\
    \reduces[\M,\ASeq]
            {\ivkBodyContext{\Svar}{f} \contextCat {\ec}}
            {\delta(f,v')}
            {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] 
            {\ec}
	    {\procClosure{\ivk}{\ivkThunk {\emptySeq}{\Svar}{f}}(a)} 
            {v}
  }
}

{\inferrule [Red FPrcd 1] {
    \reduces[\M,\ASeq] 
            {\ec}
	    {a} 
            {v'} \\
    \close{\ivk}(b,{\ivkThunk {\nmethodListVar}{\Svar}{f}}) = b' \\
    \reduces[\M,\ASeq]
            {\ivkAdvContext \contextCat {\ec}}
            {b' \subst{y}{v'}} 
            {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] 
            {\ec}
	    {\procClosure{\ivk}{\ivkThunk {(\nmethod{y}{b} \seqCat
		  \nmethodListVar)}{\Svar}{f}}
	      (a)} 
            {v}
  }
}
\end{mathpar}

\Level 4 Proceeding from Update Advice

\begin{mathpar}
{\inferrule [Red UPrcd 0] {
    \reduces[\M,\ASeq] 
            {\ec}
	    {a} 
	    {\object} \\
    l_j \in \setComp{l_i}{i \in I}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
            {\procClosure{\upd}{\updThunk {\emptySeq} {l_{j}}}
	      (a,\nmethod{x}{b})}
            {\objTempOne
              {\setComp{l_{i}=\nmethod{x_{i}}{b_{i}}}
                {i \in I \setminus j},
                l_{j} = \nmethod{x}{b}
              }
            }
  }
}

{\inferrule [Red UPrcd 1] {
    \reduces[\M,\ASeq] 
            {\ec}
	    {a} 
	    {o} \\
    \close{\upd}(b',{\updThunk {\nmethodListVar} {l_{j}}}) = b'' \\
    \reduces[\M,\ASeq] 
	    {\updAdvContext \contextCat \ec}
            {b'' {\capSubst{\mathit{rval}}{b\subst{x}{\mathit{targ}}}
		 {\mathit{targ}}}
              {\subst{\mathit{targ}}{o}}} 
            {v}
  }{%-------------------------------------------------------------
    \reduces[\M,\ASeq] {\ec}
	    {\procClosure{\upd}{\updThunk {(\nmethod{\mathit{targ}, 
		    \mathit{rval}}{b'} \seqCat \nmethodListVar)} {l_{j}}}
	      (a, \nmethod{x}{b})}
            {v}
  }
}
\end{mathpar}

\pagebreak

\Level 0 {Sample Point Cut Description Languages}

\Level 1 {Natural Selection, $M_s$}

Let $\M_{s} = \pair{\pcl[s]}{\match_s}$, where
$\pcl[s] \is \invoke{\objTempOne{\setComp{l}{}}}{l}$
and:
\[
\match_s(\advice{\invoke{\objTempOne{\setComp{l}{}}}{l}}
      {\seqComp{y}{}}{b}, \sequence{\rk,\ec,\Svar,k}) = 
\begin{cases}
\sequence{\nmethod{\seqComp{y}{}}{b}} & 
\text{if } (\rk = \ivk) \wedge (\Svar = \setComp{l}{}) \wedge (k = l)\\
\emptySeq & \text{otherwise}
\end{cases}
\]

Example:

\Level 2 {Without advice:}
\[
{\invoke{\objTempOne{\mcode{pos}=\nmethod{\mcode{p}}{\invoke{\mcode{p}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{y}}{\mcode{2}}}}{\mcode{pos}}}
\leadsto
{\mcode{2}}
\]

\Level 2 {With before advice ${\adviceTwo{\invoke{\objTempOne{\mcode{pos},\mcode{n}}}{\mcode{pos}}}{\nmethod{\mcode{x}}{\proceedivk((\updateThree{\mcode{x}}{\mcode{n}}{\nmethod{\mcode{y}}{\mcode{0}}}))}}}$:}

\[
{\invoke{\objTempOne{\mcode{pos}=\nmethod{\mcode{p}}{\invoke{\mcode{p}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{y}}{\mcode{2}}}}{\mcode{pos}}}
\leadsto
\mathNote{\mcode{0}}
\]

\Level 2 {With after advice ${\adviceTwo{\invoke{\objTempOne{\mcode{pos},\mcode{n}}}{\mcode{pos}}}{\nmethod{\mcode{x}}{\invoke{\proceedivk(\mcode{x})}{\mcode{succ}}}}}$:}

\[
{\invoke{\objTempOne{\mcode{pos}=\nmethod{\mcode{p}}{\invoke{\mcode{p}}{\mcode{n}}},\mcode{n}=\nmethod{\mcode{y}}{\mcode{2}}}}{\mcode{pos}}}
\leadsto
\mathNote{\mcode{3}}
\]

\Level 1 {General Matching, $M_G$}

\Level 2 {Allows queries over all portions of the join point abstraction.}

\Level 3 {Reduction Kind\note{: $\ivk$}}

\[
\pcl_{G} \is \VAL \syntaxOr \ivk \syntaxOr \upd \syntaxOr \ldots
\]

\Level 3 {Message\note{: $\ivk \wedge \messageIs{\mcode{pos}}$}}

\[
\pcl_{G} \is \ldots \syntaxOr \messageIs{k} \syntaxOr \ldots
\]

\Level 3 {Target signature\note{: $\ivk \wedge \messageIs{\mcode{pos}}\wedge \targetIs{\set{\mcode{pos,n}}}$}}

\[
\pcl_{G} \is \ldots \syntaxOr \targetIs{k} \syntaxOr \ldots
\]

\Level 3 {Evaluation Context\note{: $\contextIs{\mcode{.*.ib(\set{pos,n},pos)}}$}}

\[
\pcl_{G} \is \ldots \syntaxOr \contextIs{r} \syntaxOr \ldots
\]

\[
\begin{array}{p{1.5in}rcl}
\raggedleft context expr.& r & \is &
  \emptyStr \syntaxOr \ivkBodyContext{M}{m} \syntaxOr \valAdvContext
  \syntaxOr \ivkAdvContext \syntaxOr \updAdvContext \syntaxOr\\
&&&
  \wildcard \syntaxOr {r + r} 
  \syntaxOr {r r} \syntaxOr \kleeneStar{r} \\
\raggedleft signatures & M & \is & 
d \syntaxOr \setComp{l}{} \syntaxOr \wildcard \\
\raggedleft messages & m & \is & f \syntaxOr l \syntaxOr \wildcard \\
\end{array}
\]

\Level 3 {Boolean Combinations\note{: $\ivk \wedge \messageIs{\mcode{pos}}\wedge \targetIs{\set{\mcode{pos,n}}} \wedge \neg(\contextIs{\mcode{.*.ib(\set{pos,n},pos)}})$}}

\[
\pcl_{G} \is \ldots \syntaxOr {\neg\pcd} \syntaxOr {\pcd \wedge \pcd} \syntaxOr {\pcd \vee \pcd} \syntaxOr
\]

\begin{notes}
\question{To what AspectJ point cut description does this example correspond?}

\answer{\code{call(Point.pos()) \&\& !cflowbelow(call(Point.pos()))}}
\end{notes}

\Level 2 {$M_G$ is sufficient to model AspectJ}

\Level 3 {Join points}

\begin{center}
\setlength{\tabcolsep}{1.2ex}
\renewcommand{\arraystretch}{2}
\begin{tabular}{ll}
\bfseries AspectJ Point Cut & 
{\bfseries Modeled In $\pac(\M_{G})$} \\ \hline
%-------------------------------------------------------------
\code{call(void Point.pos())} & 
\note{$\ivk \wedge \targetIs{\set{\mcode{n,pos}}} \wedge 
  {\messageIs{\mcode{pos}}}$}\\ 
%-------------------------------------------------------------
\code{call(Point.new())} &
\note{$\VAL \wedge \targetIs{\set{\mcode{n,pos}}}$} \\ 
%-------------------------------------------------------------
\code{execution(void Point.pos())} &
\note{$\VAL \wedge 
  {\contextIs{\ivkBodyContext{\set{\mcode{n,pos}}}
      {\mcode{pos}} \kleeneStar{\wildcard}}}$} \\ 
%-------------------------------------------------------------
\code{get(int Point.n)} &
\note{$\ivk \wedge \targetIs{\set{\mcode{n,pos}}} \wedge 
  {\messageIs{\mcode{n}}}$}\\ 
%-------------------------------------------------------------
\code{set(int Point.n)} &
\note{$\upd \wedge \targetIs{\set{\mcode{n,pos}}} \wedge 
  {\messageIs{\mcode{n}}}$}\\ 
%-------------------------------------------------------------
\code{adviceexecution()} &
\note{$\contextIs{\kleeneStar{\wildcard}
    (\valAdvContext + \ivkAdvContext + \updAdvContext)
    \kleeneStar{\wildcard}
  }$}
\\ 
%-------------------------------------------------------------
\code{within(Point)} &
\note{$\contextIs{
  \ivkBodyContext{\set{\mcode{n,pos}}}{\wildcard}
  \kleeneStar{\wildcard}
}$}
\\ 
%-------------------------------------------------------------
\code{withincode(Point.pos)} &
\note{$\contextIs{
  \ivkBodyContext{\set{\mcode{n,pos}}}{\mcode{pos}}
  \kleeneStar{\wildcard}
}$}
\\ 
%-------------------------------------------------------------
\code{cflow(Point.pos)} &
\note{$\contextIs{\kleeneStar{\wildcard} 
    \ivkBodyContext{\set{\mcode{n,pos}}}{\mcode{pos}}
    \kleeneStar{\wildcard}}$} \\ 
%-------------------------------------------------------------
\code{cflowbelow(Point.pos)} &
\note{$\contextIs{\kleeneStar{\wildcard}
\wildcard
\ivkBodyContext{\set{\mcode{n,pos}}}{\mcode{pos}}
\kleeneStar{\wildcard}}$} \\
%-------------------------------------------------------------
\code{this(Point)} &
\note{$\contextIs{
  \ivkBodyContext{\set{\mcode{n,pos}}}{\wildcard}
  \kleeneStar{\wildcard}
}$}
\\ 
%-------------------------------------------------------------
\code{target(Point)} &
\note{$\targetIs{\set{\mcode{n,pos}}}$}
\\ \hline
%-------------------------------------------------------------
\end{tabular}
\end{center}

\question{Does cflowbelow consider advice execution to be ``below'' a cflow?}

\question{Does our model?}

\begin{notes}
\answer{Yes}

\question{What if it should not be?}

\answer{$\contextIs{\kleeneStar{\wildcard}
\ivkBodyContext{\wildcard}{\wildcard}
\ivkBodyContext{\set{\mcode{n,pos}}}{\mcode{pos}}
\kleeneStar{\wildcard}}$}
\end{notes}

\question{What about the variable binding form of \code{this}?}

\note{\answer{Would need to change core calculus to track \code{this} in
  evaluation context.}}

\question{What else is missing?}

\begin{notes}
\answer{Non-sensical: Constructor advice, initialization advice,
  handler advice, args point cut}

\answer{Omitted: if (but could be handled in PCDL without changing
  core calculus)}
\end{notes}

\homework{Are there interesting things that can be said in $M_G$ that
would give insight into join points ``missing'' from AspectJ?}

\Level 3 {Open Classes (a.k.a.~intertype declarations)}

\begin{program}
int Point.color = 0;
\end{program}

A model of this in $\M_G$ uses two pieces of advice:

\begin{program}
$(\VAL \wedge \targetIs{\set{\mcode{n,pos}}}) \rhd \s()$\\
\>\ralb orig=\s(s)\proceedval(), \\
\>n=\s(s)s.orig.n,\\
\>pos=\s(s)s.orig.pos, color=\s(s)0\larb \pnp
$(\upd \wedge \targetIs{\set{\mcode{orig,n,pos,color}}} \wedge 
(\messageIs{\mcode{n}} \vee \messageIs{\mcode{pos}})) \rhd$\\
\>\s(t,r) \>\>\>\ralb orig=\s(s)\proceedupd(t.orig, \s(t)r),\\
\>\>\>\>n=\s(s)s.orig.n,\\
\>\>\>\>pos=\s(s)s.orig.pos, color=\s(s)t.color\larb
\end{program}

\question{Why is the second piece of advice needed?}

\note{\answer{Consider an invocation after an update if we just have
    the first piece of advice.}}

\Level 1 {Other Models}

\Level 2 {Modeling HyperJ}

\Level 3 {Can use $M_G$}

\Level 3 {Like Open Classes, but two key differences:}

\Level 4 {Special basic constants represent module names}

\Level 4 {A model for abstact methods allows composed modules to call
  each other while remaining oblivious to the other module's
  implementation}

\Level 2 {Modeling Adaptive Methods}

\Level 3 {Basic Idea}

Adaptive methods allow a \note{declarative} specification of a
\note{traversal strategy} over an \note{object graph}.

Specify:

\begin{itemize}
\item {\note{links to be traversed in object graph}}

\item {\note{actions to performed at each node in the graph}}
\end{itemize}

Example: \note{\code{for each Employee e of each CostCenter c: total
    += e.salary()}}

\Level 3 {Is $M_G$ sufficient?}

\note{Need mechanism to find fields of an object that are not known
  when the advice is written.  \emph{Reflection}}

\Level 3 {Keys to model in \pac}

\Level 4 {Use distinguished names to indicate fields of objects}

\Level 4 {Extend $M_G$ with \note{reflection}}

\note{$\forall f \in \mcode{fieldsOf(S)}$}

\note{Matching advice returns $n$ copies of the advice body, for a
  target object with $n$ fields.}

\Level 4 {Use the two parameters of update advice in a unique way}

\Level 5 {Target object is used for dispatching to the appropriate
  code for the node}

\Level 5 {R-value is used to pass a visitor (accumulator) object}

\Level 1 {Insights}

\Level 2 {Spectators and Assistants}

\question{Can we study them using \pac?}

\question{How might we add imperative features?}

\question{Can we eliminate any features from \pac?  Should we?}

\Level 2 {Interaction of PCDL and base language}

\question{How does the design of the PCDL effect reasoning in the base
language?}

\Level 2 {Comparisons}

\question{What do we learn about similarities between the modeled langauges?}

\question{Differences?}

\Level 1 {Decisions in the design of \pac}

\Level 2 {Big step or little step?}

\Level 2 {Functional or imperative?}

\Level 2 {Include constants?}

\Level 2 {Advice declarations or terms? \note{Advice scoping}}

\end{Outline}

\pagebreak

\bibliographystyle{abbrv}
\bibliography{all,web}

\end{document}