\documentclass[landscape]{seminar}
\usepackage{alltt,graphicx,fixseminar,latexsym,color}
%
\newenvironment{Maude}[1]
{\begin{center}\begin{minipage}{#1}\begin{alltt}}
{\end{alltt}\end{minipage}\end{center}}

\newenvironment{Slide}[1]
{
\begin{slide}
\sf
\begin{center}
\textcolor{cyan}{\Large\em #1}
\end{center}
}
{
\end{slide}
}
\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\EM}[1]{\textcolor{red}{\em #1}}
%
\begin{document}

\begin{Slide}{\huge The Maude 2.0 System}
\begin{center}
\vspace{0.5in}
M. Clavel\ \ \ \ F. Dur\'{a}n\ \ \ \ S. Eker\ \ \ \ P. Lincoln\\
\vspace{.2in}
N. Mart\'{\i}-Oliet\ \ \ \ J. Meseguer\ \ \ \ C. Talcott 
\end{center}
\end{Slide}


\begin{Slide}{Overview}
\begin{itemize}
\item Maude is a language based on rewriting logic.
\item Type system is based on membership equation logic.
\item Equations are assumed to be confluent and terminating; 
used for conventional algebraic specification \& functional
programming.
\item Rewrite rules are assume to be coherent w.r.t. equations (Viry);
used to express inference \& state change.
\item Maude modules themselves form an algebraic data type -
metaprogramming; extension via reflection .
\item Can be used as a semantic framework to specify \& prototype
other languages and as a logical framework to represent \& mechanize
other logics.
\item Maude 2.0 is the latest incarnation.
\end{itemize}
\end{Slide}


\begin{Slide}{New Term Representation}
\begin{itemize}
\item Supports AC, ACU, A, AU.
\item Based on persistent data structures.
\item Reduces the computational complexity of $E$-rewriting for large
subjects and simple patterns.
\end{itemize}
\vspace{0.15in}
\begin{Maude}{3.5in}
fmod REV-LIST is
  sort List Elt .  subsort Elt < List .
  op nil : -> List .
  op __ : List List -> List [assoc id: nil] .
  ops a b c d e : -> Elt .
  vars E E2 : Elt .  var L : List .
\end{Maude}
\end{Slide}


\begin{Slide}{New Term Representation (2)}
\begin{Maude}{3.5in}
  op rev : List -> List .
  eq rev(nil) = nil .
  eq rev(E L) = rev(L) E .

  op rev2 : List -> List .
  eq rev2(nil) = nil .
  eq rev2(E) = E .
  eq rev2(E L E2) = E2 rev2(L) E .

  op rev3 : List -> List .
  eq rev3(nil) = nil .
  eq rev3(L E) = E rev3(L) .
endfm
\end{Maude}
\begin{itemize}
\item All three naive list reversal algorithms run in linear time!
\end{itemize}
\end{Slide}


\begin{Slide}{Conditions}
\begin{itemize}
\item Rather than a single equality, conditions now allow a list of
\EM{condition fragments}, separated by \textcolor{red}{$/\backslash$}.
\item 4 types of fragments; last type is for rule conditions only:
\end{itemize}
\begin{center}
\begin{tabular}{|l|l|}
\hline
$\la$term$\ra$ = $\la$term$\ra$ & equality test \\
\hline
$\la$term$\ra$ : $\la$sort$\ra$ & sort test \\
\hline
$\la$pattern$\ra$ := $\la$term$\ra$ & assignment by matching \\
\hline
$\la$term$\ra$ $=>$ $\la$pattern$\ra$ & rewrite proof search \\
\hline
\end{tabular}
\end{center}
\begin{itemize}
\item Patterns may have unbound variables that are bound by matching;
regular terms are reduced upto strategy.
\item Failure of a fragment causes backtracking.
\end{itemize}
\end{Slide}



\begin{Slide}{Iter Attribute}
\begin{itemize}
\item Allows efficient storage, i/o and sort computations for huge
towers of unary operator symbols.
\item Main application is the efficient implementation of natural
numbers using the successor notation.
\end{itemize}
\begin{Maude}{3in}
fmod ITER-TEST is
  sorts Even Odd Nat .
  subsorts Even Odd < Nat .
  op 0 : -> Even .
  op s_ : Even -> Odd [iter] .
  op s_ : Odd -> Even [iter] .
endfm

red s_^123456789(0) .
red s_^1234567890(0) .
\end{Maude}
\end{Slide}


\begin{Slide}{Natural Numbers}
\begin{itemize}
\item Nats are constructed using successor operator and the \EM{iter}
attribute.
\end{itemize}
\begin{Maude}{3.3in}
fmod NAT is
  sorts Zero NzNat Nat .
  subsort Zero NzNat < Nat .
  op 0 : -> Zero [ctor] .
  op s_ : Nat -> NzNat
    [ctor iter special (...)] .
  ...
endfm
\end{Maude}
\begin{itemize}
\item Decimal i/o by default.
\item Built-in operators very efficient (use GNU GMP).
\item Gcd, lcm, mod exp, bitwise ops.
\end{itemize}
\end{Slide}


\begin{Slide}{Natural Numbers (continued)}
\begin{Maude}{3.3in}
red in NAT : gcd(18, gcd(X:Nat, 12)) .

fmod COMBINATORIAL is protecting NAT .
  op _! : Nat -> NzNat .
  op C : Nat Nat -> Nat .

vars N M : Nat .
  eq 0 ! = s 0 .
  eq (s N) ! = s N * N ! .
  eq C(N, M) = N ! quo (M ! * sd(N, M) !) .
endfm

red 1000 ! .
red C(1000, 100) .
\end{Maude}
\end{Slide}


\begin{Slide}{Other Built-ins}
\begin{itemize}
\item Integers (constructed from Nats).
\begin{Maude}{3.3in}
subsorts NzNat < NzInt Nat < Int .
op -_ : NzNat -> NzInt [...] .
\end{Maude}
\item Rationals (constructed from Ints and Nats).
\begin{Maude}{3.3in}
subsorts NzInt < NzRat Int < Rat .
op _/_ : NzInt NzNat -> NzRat [...] .
\end{Maude}
\item IEEE Floating Point Numbers.
\item Strings (using SGI Rope package).
\item Comprehensive set of conversion functions.
\end{itemize}
\end{Slide}


\begin{Slide}{LTL Model Checker}
\begin{itemize}
\item Linear Temporal Logic manipulations (simplifications and
negative normal form) are done by Maude code.
\item The satisfaction of (possibly parameterized) propositions are
defined in Maude.
\item On-the-fly model checking is done by a built-in operation
\end{itemize}
\begin{Maude}{3.3in}
op modelCheck : State Formula ~> ModelCheckResult
  [special (...)] .
\end{Maude}
\begin{itemize}
\item Implementation uses state-of-the-art Buchi automaton construction
algorithm and standard double depth first search of the synchronous
product for a counterexample.
\item LTL Satisfiability solving and tautology checking also provided.
\end{itemize}
\end{Slide}


\begin{Slide}{New Meta Level}
\begin{itemize}
\item Simpler metaterm representation:
\begin{Maude}{3.3in}
1.0 + X:Float
\end{Maude}
is meta-represented as
\begin{Maude}{3.3in}
'_+_['1.0.FiniteFloat, 'X:Float]
\end{Maude}
\item Many more descent functions such as metaXapply() (with contexts)
and metaSearch().
\item Descent functions return sorts of terms.
\item Ascent functions to inspect modules in database.
\item Much more sophisticated caching at module and operator level.
\end{itemize}
\end{Slide}


\begin{Slide}{Term Coloring}
\begin{itemize}
\item Color (possibly intermediate) results based on reduced flag and
constructor status to flag problems.
\end{itemize}
\begin{Maude}{3.3in}
set print color on .
\end{Maude}
\begin{center}
\begin{tabular}{|l|l|}
\hline
reduced, ctor &	not colored \\
\hline
reduced, non-ctor, colored below & \textcolor{blue}{blue} \\
\hline
reduced, non-ctor, no colored below & \textcolor{red}{red} \\
\hline
unreduced, no reduced above & \textcolor{green}{green} \\
\hline
unreduced, reduced directly above & \textcolor{magenta}{magenta} \\
\hline
unreduced, reduced not directly above & \textcolor{cyan}{cyan} \\
\hline
\end{tabular}
\end{center}
\begin{itemize}
\item \textcolor{red}{Red} and \textcolor{magenta}{magenta} denote
likely origin of problem, \textcolor{blue}{blue} and
\textcolor{cyan}{cyan} denote secondary damage.
\end{itemize}
\end{Slide}


\begin{Slide}{Format Attribute}
\begin{itemize}
\item Allows control of white-space, color and style for pretty-printing
operators.
\item Format words are given for each white-space position.
\end{itemize}
\scriptsize
\begin{center}
\begin{tabular}{|ll|ll|ll|}
\hline
s & space & r & red & R & background red \\
\hline
t & tab & g & green & G & background green \\
\hline
+ & increment indent counter & b & blue & B & background blue \\
\hline
- & decrement indent counter & y & yellow & Y & background yellow \\
\hline
i & indent by indent counter & m &  magenta & M & background magenta \\
\hline
n & new line & c & cyan & C & background cyan \\
\hline
f & flash & w & white & W & background white \\
\hline
h & hidden & p & black & P & background black \\
\hline
d & default spacing & u & underline & x & reverse video \\
\hline
o & original style & ! & bright & ? & dim \\
\hline
\end{tabular}
\end{center}
\end{Slide}


\begin{Slide}{Format Attribute (2)}
\begin{Maude}{3.75in}
op while _ do _ od : Bool Statement -> Statement . 
  ^     ^ ^  ^ ^  ^

op let _ := _ : Variable Expression -> Statement .
  ^   ^ ^  ^ ^
\end{Maude}
\vspace{0.25in}
\begin{Maude}{3.75in}
op while _ do _ od : Bool Statement -> Statement
  [format (nir! o r! o++ --nir! o)] .

op let _ := _ : Variable Expression -> Statement
  [format (nir! o d d d)] .
\end{Maude}
\end{Slide}


\begin{Slide}{Other New Features}
\begin{itemize}
\item Profiling.
\item Break points (on symbols or labeled statements).
\item Rewrite search, dump of rewrite graph.
\item Kind level declarations \& on-the-fly variable declarations.
\item Command line editing (Tecla).
\item Frozen attribute.
\item Position fair \& object-message rewriting.
\item Statement attributes: owise, label, nonexec, metadata.
\item Optimizations: left-to-right sharing, order sorted
  discrimination nets, substitution slot coloring.
\item More powerful module operations in Full Maude.
\end{itemize}
\end{Slide}


\begin{Slide}{Availability}
Runs under Unix (all flavors).

Licensed under GNU GPL.

Source tree, manual, examples and binaries for selected architectures
available from the new Maude website:
\begin{center}
\Huge
\textcolor{red}{http://maude.cs.uiuc.edu/}
\end{center}
\end{Slide}

\end{document}
