\documentclass{beamer}
\usetheme[style=plain]{uu}

%% unicode support, for text and code :)
\usepackage[utf8x]{inputenc}
\usepackage{ucs}
\usepackage{autofe}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{color}


%% Haskell syntax highlighting and code font
\usepackage{minted}
\usepackage{fancyvrb}
\usemintedstyle{default}
\newminted{haskell}{gobble=8,xleftmargin=42pt,linenos,mathescape,fontfamily=tt,fontsize=\footnotesize}



%% Metainformation
%% PDF stuff
\usepackage{datetime}
\usepackage{ifpdf}
\ifpdf
\pdfinfo{
    /Author (J.P.PizaniFlor)
    /Title (Weakest pre-condition calculus for Lang0)
    /Keywords (Hoare Logic, Weakest Pre-Condition, Haskell, Formal methods, Program verification)
    /CreationDate (D:\pdfdate)
}
\fi

\title[wp-lang0]{Weakest pre-condition calculus for Lang0}
\subtitle{Program Verification - 2012/2013}

\date{\today}

\author[Pizani Flor]
{
    João Paulo Pizani Flor
}

\institute[Utrecht University]
{
    Department of Information and Computing Sciences,
    Utrecht University
}

\subject{Program Verification}




%% The document itself
\begin{document}

%% Code excerpts
\defverbatim[colored]\haskellLangZero{
    \begin{haskellcode}
        data L0Value = I Integer | B Bool

        data L0Instruction
            = SetLocal Int L0Value | LoadLocal Int
            | StoreLocal Int | LoadParam Int
            | StoreParam Int | PushLiteral L0Value | Pop
            | L0Add | L0Sub | L0Mul | L0Div | L0Equ
            | L0Lt | L0Gt | L0Lte | L0Gte | L0Return

        data L0Statement
            = Inst L0Instruction
            | IfThenElse L0Statement L0Statement
            | Stmts [L0Statement]

        type PName = String
        type NPar  = Int
        type NLoc  = Int
        data L0Program = L0Program PName NPar NLoc L0Statement
    \end{haskellcode}
}

\defverbatim[colored]\haskellSpecZero{
    \begin{haskellcode}
        type Variable = Char

        data Sp0Expr
            = Return | Var Variable | Integer Integer
            | Boolean Bool | Param Int | Local Int | Stack Int
            | Add Sp0Expr Sp0Expr | Sub Sp0Expr Sp0Expr
            | Mul Sp0Expr Sp0Expr | Div Sp0Expr Sp0Expr
            | Aeq Sp0Expr Sp0Expr | Lt  Sp0Expr Sp0Expr
            | Lte Sp0Expr Sp0Expr | Gt  Sp0Expr Sp0Expr
            | Gte Sp0Expr Sp0Expr

        data Sp0Formula
            = Verum | Falsum | Exp Sp0Expr | Not Sp0Formula
            | And Sp0Formula Sp0Formula
            | Or Sp0Formula Sp0Formula
            | Implies Sp0Formula Sp0Formula
            | Exists Variable Sp0Formula
            | ForAll Variable Sp0Formula
    \end{haskellcode}
}

\defverbatim[colored]\haskellWpTop{
    \begin{haskellcode}
        wp :: L0Program -> Sp0Formula -> Sp0Formula
        wp (L0Program _ _ _ body) q = wp_ body q

        wp_ :: L0Statement -> Sp0Formula -> Sp0Formula
        wp_ (Inst i)         q = wp_inst  i  q
        wp_ (Stmts ss)       q = wp_stmts ss q
        wp_ (IfThenElse t e) q = theni `And` elsei
            where theni   = stackZe     `Implies` wp_ t q
                  elsei   = Not stackZe `Implies` wp_ e q
                  stackZe = Exp $ Aeq (Stack 0) (Integer 0)

        wp_stmts :: [L0Statement] -> Sp0Formula -> Sp0Formula
        wp_stmts [x] q      = wp_ x q
        wp_stmts (x:z:zs) q = wp_ x (wp_stmts (z:zs) q)
    \end{haskellcode}
}

\defverbatim[colored]\haskellWpInst{
    \begin{haskellcode}
        wp_inst :: L0Instruction -> Sp0Formula -> Sp0Formula
        wp_inst (SetLocal k v) q = rewr (localToLit   k v) q
        wp_inst (LoadLocal k)  q = rewr (stackToLocal 0 k) q
        wp_inst (StoreParam k) q = rewr (paramToStack k 0) q
        wp_inst Pop            q = rewr (stackToStack 0 1) q
        wp_inst L0Return       q = rewr returnToStack      q
        ...

        returnToStack :: Sp0Expr -> Sp0Expr
        returnToStack e = if isReturn e then (Stack 0) else e

        type BinOperator = Sp0Expr -> Sp0Expr -> Sp0Expr

        binOpTransform :: BinOperator -> Sp0Expr -> Sp0Expr
        binOpTransform op e
            | isStack e ((==) 0) = op (Stack 0) (Stack 1)
            | otherwise          = e
    \end{haskellcode}
}



    \begin{frame}
        \titlepage
    \end{frame}

    \begin{frame}
        \frametitle{Table of Contents}
        \tableofcontents
    \end{frame}

    \section{The languages}
    \label{sec:languages}

        \subsection{Lang0}
        \label{subsec:lang0}
            \begin{frame}
                \frametitle{The Lang0 language datatype}
                \haskellLangZero
            \end{frame}

        \subsection{Spec0}
        \label{subsec:spec0}
            \begin{frame}
                \frametitle{The Spec0 language datatype}
                \haskellSpecZero
            \end{frame}

    \section{WP calculus for Lang0}
    \label{sec:wpcalc}

        \subsection{Top-level}
        \label{subsec:tlwpcalc}
            \begin{frame}
                \frametitle{WP rules for (compound) statements}
                \haskellWpTop
            \end{frame}

        \subsection{Some instructions}
        \label{subsec:instwpcalc}
            \begin{frame}
                \frametitle{WP rules for (some) instructions}
                \haskellWpInst
            \end{frame}

    \section{Tools}
    \label{sec:tools}

        \begin{frame}
            \frametitle{Tools}
            \begin{description}
                \item[Programming language] Haskell
                \newline

                \item[Theorem prover] Z3 (Microsoft Research)
                \newline

                \item[Language bindings] The \texttt{z3} package (on hackage)
                \begin{itemize}
                    \item Haskell bindings for Z3
                    \item High-level API
                    \item We need to translate values from our \texttt{Spec0}
                        type to \texttt{Z3.Lang.Prelude.\{Expr,Z3\}}
                \end{itemize}
            \end{description}
        \end{frame}


\end{document}
