test-newExporter.tex

% Created 2015-08-31 Mon 12:25
\documentclass[compress,notes=hide]{beamer}
\mode<presentation>
{
  \usetheme{Madrid}\useinnertheme{default}
  \setbeamercovered{transparent}}
\makeatletter
\setbeamertemplate{footline}
{
  \leavevmode%
  \hbox{%
  \begin{beamercolorbox}[wd=.333333\paperwidth,ht=2.25ex,dp=1ex,center]{author in head/foot}%
    \usebeamerfont{author in head/foot}\insertsection
  \end{beamercolorbox}%
  \begin{beamercolorbox}[wd=.333333\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}%
    \usebeamerfont{title in head/foot}\insertsubsection
  \end{beamercolorbox}%
  \begin{beamercolorbox}[wd=.333333\paperwidth,ht=2.25ex,dp=1ex,right]{date in head/foot}%
    \usebeamerfont{date in head/foot}\insertshortdate{}\hspace*{2em}
    \insertframenumber{} / \inserttotalframenumber\hspace*{2ex}
  \end{beamercolorbox}}%
  \vskip0pt%
}
\makeatother
\usepackage[english]{babel}
\usepackage{times}
\usepackage{pgf}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fixltx2e}
\usepackage{graphicx}
\usepackage{longtable}
\usepackage{float}
\usepackage{wrapfig}
\usepackage{rotating}
\usepackage[normalem]{ulem}
\usepackage{amsmath}
\usepackage{textcomp}
\usepackage{marvosym}
\usepackage{wasysym}
\usepackage{amssymb}
\usepackage{hyperref}
\tolerance=1000
\usepackage{colonequals}
\usepackage[noend]{algorithmic}
\usepackage{bussproofs}
\usepackage{nicefrac}
\institute{Department of Mathematical Sciences\\University of Puerto Rico at Mayagüez\\Mayagüez, PR}
\author{Marko Schütz-Schmuck}
\date{\today}
\title{Example Correctness Proofs}
\hypersetup{
  pdfkeywords={},
  pdfsubject={},
  pdfcreator={Emacs 24.3.1 (Org mode 8.2.4)}}
\begin{document}

\maketitle

\include{extra-setup}

\section{linear search}
\label{sec-1}
\begin{itemize}
\item sought: smallest index \(i\) with \(a_i = x\)
\item precondition: \(V \equiv n \in \naturals_0\)
\item postcondition:
\begin{align*}
P \equiv & n \in \naturals_0 \land k \in \naturals \land k \le n+1
\land \textmath{found} \in \booleans \\
& \land \forall 1 \le i < k.a_i \neq x \\
& \land (k \le n \land a_k = x \land \textmath{found} \lor k = n+1 \land \neg \textmath{found})
\end{align*}
\end{itemize}

\begin{enumerate}
\item verify\hfill{}\textsc{BMCOL:B_block}
\label{sec-1-1}

\begin{minipage}{.9\linewidth}
\(
\begin{Condition}
V
\end{Condition}\)\endgraf
\begin{Pseudocode}
\STATE \(k \isassigned 1\)
\WHILE{\(k \le n \land a_k \neq x\)} \STATE \(k \isassigned k+1\) \ENDWHILE
\STATE \(\textmath{found} \isassigned k \le n\)
\end{Pseudocode}
\(
\begin{Condition}
P
\end{Condition}\)
\end{minipage}
\item invariant\hfill{}\textsc{B_block:BMCOL}
\label{sec-1-2}
\begin{align*}
& n \in \naturals_0 \land k \in \naturals_0 \land k \le n+1 \\
& \land \forall 1\le i<k. a_i
\neq x
\end{align*}
\end{enumerate}
\section{proof overview}
\label{sec-2}
\(
\begin{Condition}
V
\end{Condition}\)\endgraf
\begin{Pseudocode}
\STATE \(k \isassigned 1\)
\WHILE{\(k \le n \land a_k \neq x\)} \STATE \(k \isassigned k+1\) \ENDWHILE
\STATE \(\textmath{found} \isassigned k \le n\)
\end{Pseudocode}
\(
\begin{Condition}
P
\end{Condition}\)

{\tiny
\begin{prooftree}
\AxiomC{\(V \implies I\substitute{1}{k}\)}
\RightLabel{A2}
\UnaryInfC{\hoareTriple{V}{\(S_i\)}{I}}
\AxiomC{\(I \land B \implies I\substitute{k+1}{k}\)}
\RightLabel{A2}
\UnaryInfC{\hoareTriple{I \land B}{\(S_W\)}{I}}
\AxiomC{\(I \land \neg B \implies P_1\)}
\RightLabel{W2}
\TrinaryInfC{\hoareTriple{V}{\(S_i\ \algorithmicseq\ W\)}{P_1}}
\AxiomC{\hoareTriple{P\substitute{k\le n}{\textmath{found}}}{\(S_f\)}{P}}
\RightLabel{A1}
\UnaryInfC{\hoareTriple{P_1}{\(S_f\)}{P}}
\RightLabel{S1}
\BinaryInfC{\hoareTriple{V}{\(S_i\ \algorithmicseq\ W\ \algorithmicseq\ S_f\)}{P}}
\end{prooftree}
}

termination: distance \(n+1 - k\)
\section{strengthen postcondition of loop body}
\label{sec-3}
\begin{itemize}
\item rule (P1) allows strengthening postcondition
\item may make proving easier
\end{itemize}

\section{merge sorted sub-sequences}
\label{sec-4}
\begin{itemize}
\item given: arrays \(a, b, c\) with \(a, b\) sorted by value
\item merge the sorted sequences of values into a sorted sequence of values in \(c\)
\item precondition:
\begin{align*}
V \equiv & n_a \in \naturals_0 \land \forall 1 \le i < n_a . a_i \le a_{i+1} \\
  \land & n_b \in \naturals_0\land \forall 1 \le i < n_b . b_i \le b_{i+1}
\end{align*}
\item predicate for permutations: \([] \perm []\), \(a \& b \& c \perm d \& b \& e \iff a \&
    c \perm d \& e\) where \(\&\) has precedence over \(\perm\)
\item postcondition:
\begin{align*}
P \equiv & \appendop_{i=1}^{n_a+n_b} [c_{i}] \perm \appendop_{i=1}^{n_a} [a_i] \&
\appendop_{i=1}^{n_b} [b_i]\\
\land & \forall 1 \le i < n_a+n_b . c_i \le c_{i+1}
\end{align*}
\end{itemize}

\section{proof obligations: black-box view}
\label{sec-5}
\begin{enumerate}
\item \hoareTriple{V}\{\(\textmath{merge}\)\}\{P\}
\item \(\textmath{merge}(d)\) is structurally like \(d\)
\item \(\textmath{merge}\) will not modify any program variables other than \(c_i\) where
     \(1 \le i \le n_a+n_b\)
\item \(\textmath{merge}\) terminates
\end{enumerate}

\section{merge subprogram}
\label{sec-6}
\begin{algorithmic}
\DECLARE \((i_a, \naturals, 1), (i_b, \naturals, 1), (i_c, \naturals, 1)\)
\WHILE{\(i_a \le n_a \lor i_b \le n_b\)}
\IF{\(i_b > n_b \lor i_a \le n_a \land a_{i_a} \le b_{i_b}\)}
\STATE \(c_{i_c} \isassigned a_{i_a}\)
\STATE \(i_a \isassigned i_a + 1\)
\ELSE
\STATE \(c_{i_c} \isassigned b_{i_b}\)
\STATE \(i_b \isassigned i_b + 1\)
\ENDIF
\STATE \(i_c \isassigned i_c +1\)
\ENDWHILE
\RELEASE \(i_a, i_b, i_c\)
\end{algorithmic}
\section{proof obligations: looking under the hood}
\label{sec-7}
\begin{enumerate}
\item $\backslash$(
\begin{Condition}
V
\end{Condition}$\backslash$)
\begin{Pseudocode}
\DECLARE \((i_a, \naturals, 1), (i_b, \naturals, 1), (i_c, \naturals,
1)\)
\WHILE{\(i_a \le n_a \lor i_b \le n_b\)}
\IF{\(i_b > n_b \lor i_a \le n_a \land a_{i_a} \le b_{i_b}\)}
\STATE \(c_{i_c} \isassigned a_{i_a}\)
\STATE \(i_a \isassigned i_a + 1\)
\ELSE
\STATE \(c_{i_c} \isassigned b_{i_b}\)
\STATE \(i_b \isassigned i_b + 1\)
\ENDIF
\STATE \(i_c \isassigned i_c +1\)
\ENDWHILE
\RELEASE \(i_a, i_b, i_c\)
\end{Pseudocode}
$\backslash$(
\begin{Condition}
P
\end{Condition}$\backslash$)

\item maintains structure

\item only modifies \(c_i\) where \(1 \le i \le n_a+n_b\)
\end{enumerate}
\section{proving \hoareTriple{V}\{\(\textmath{merge}\)\}\{P\}}
\label{sec-8}
\begin{itemize}
\item invariant: \(I \equiv \bigvee_{i=0}^8 I_i\) where
\begin{description}
\item[{\(I_0 \equiv\)}] \(n_a \in \naturals_0 \land n_b \in \naturals_0\)
\item[{\(I_1 \equiv\)}] \(i_a \in \naturals_0 \land 1\le i_a\le n_a+1\)
\item[{\(I_2 \equiv\)}] \(i_b \in \naturals_0 \land 1\le i_b\le n_b+1\)
\item[{\(I_3 \equiv\)}] \(i_c-1 = i_a - 1 + i_b - 1\)
\item[{\(I_4 \equiv\)}] \(\appendop_{i=1}^{i_c-1} [c_{i}] \perm \appendop_{i=1}^{i_a-1} [a_i] \&
      \appendop_{i=1}^{i_b - 1} [b_i]\)
\item[{\(I_5 \equiv\)}] \((1 < i_c \land i_a \le n_a) \implies c_{i_c-1} \le a_{i_a}\)
\item[{\(I_6 \equiv\)}] \((1 < i_c \land i_b \le n_b) \implies c_{i_c-1} \le b_{i_b}\)
\item[{\(I_7 \equiv\)}] \(\forall 1 \le i < i_c-1 . c_i \le c_{i+1}\)
\item[{\(I_8 \equiv\)}] \(\forall 1 \le i < n_a . a_i \le a_{i+1} \land \forall 1
                        \le i < n_b . b_i \le b_{i+1}\)
\end{description}
\item symmetric wrt. renaming \(a \leftrightarrow b\)
\end{itemize}
\section{proof overview}
\label{sec-9}
{\tiny
\begin{prooftree}
\AxiomC{\(V \implies I\substitute{1,1,1}{i_c,i_b,i_a}\)}
\RightLabel{S1\(^+\), D1}
\UnaryInfC{\hoareTriple{V}{\(\textmath{init}\)}{I}}
\end{prooftree}
}
\begin{itemize}
\item \(B_1 \land B_2 \iff i_a\le n_a \land (i_b > n_b \lor a_{i_a}\le b_{i_b})\) and \(B_1
    \land \neg B_2 \iff i_b\le n_b \land (i_a > n_a \lor b_{i_b} < a_{i_a})\)
\end{itemize}
{\tiny
\begin{prooftree}
\AxiomC{\(\vdots\)}
\UnaryInfC{\hoareTriple{I \land B_1 \land B_2}{\(S_1\)}{I\substitute{i_c+1}{i_c}}}
\AxiomC{\(I \land i_b\le n_b \land (i_a > n_a \lor b_{i_b} \le a_{i_a}) \implies I\substitute{i_c+1,i_b+1,b_{i_b}}{i_c,i_b,c_{i_c}}\)}
\RightLabel{S1, A1, A2}
\UnaryInfC{\hoareTriple{I \land i_b\le n_b \land (i_a > n_a \lor b_{i_b} \le a_{i_a})}{\(S_1\)}{I\substitute{i_c+1}{i_c}}}
\RightLabel{P1}
\UnaryInfC{\hoareTriple{I \land i_b\le n_b \land (i_a > n_a \lor b_{i_b} < a_{i_a})}{\(S_1\)}{I\substitute{i_c+1}{i_c}}}
\UnaryInfC{\hoareTriple{I \land B_1 \land \neg B_2}{\(S_2\)}{I\substitute{i_c+1}{i_c}}}
\RightLabel{IF1}
\BinaryInfC{\hoareTriple{I \land B_1}{\(S\)}{I\substitute{i_c+1}{i_c}}}
\end{prooftree}
}
{\tiny
\begin{prooftree}
\AxiomC{\hoareTriple{V}{\(\textmath{init}\)}{I}}
\AxiomC{\hoareTriple{I \land B_1}{\(S\)}{I\substitute{i_c+1}{i_c}}}
\RightLabel{S1, A1}
\UnaryInfC{\hoareTriple{I \land B_1}{\(S\ \algorithmicseq\ i_c \isassigned i_c + 1\)}{I}}
\AxiomC{\(I \land \neg B_1 \implies P\)}
\RightLabel{W2}
\TrinaryInfC{\hoareTriple{V}{\(\textmath{init}\ \algorithmicseq\ W\)}{P}}
\AxiomC{}
\RightLabel{SP1}
\UnaryInfC{\hoareTriple{P}{\(R\)}{P}}
\RightLabel{S1}
\BinaryInfC{\hoareTriple{V}{\(\textmath{init}\ \algorithmicseq\ W\ \algorithmicseq\ R\)}{P}}
\end{prooftree}
}
% Emacs 24.3.1 (Org mode 8.2.4)
\end{document}