\usepackage{pstricks,pst-node}
\usepackage{amssymb}
\usepackage{amsmath}

\newcommand{\hi}[1]{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Titles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\stitle}[2]{\underline{{\bf #1}: #2}}
\newcommand{\stitles}[1]{\underline{\bf #1}}
\newcommand{\largetitle}[1]{
  \begin{center}
    {\large{\fbox{#1}}}
  \end{center}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Language and Structure
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\memph}[1]{\mbox{\emph{#1}}}

\newcommand{\conceptbox}[2]{
  #1
  \hspace*{2em}\begin{minipage}[t]{27em}
  #2
  \end{minipage} \\
}

\newcommand{\google}[1]{\small {\tt Google} search: {\tt #1}}

\newcommand{\problem}{{\bf Problem}}
\newcommand{\solution}{{\bf Solution}}
\newcommand{\given}{{\bf Given}}
\newcommand{\instance}{{\bf Instance}}
\newcommand{\example}{{\bf Example}}
\newcommand{\remark}{{\bf Remark}}
\newcommand{\recall}{{\bf Recall}}
\newcommand{\exercise}{{\bf Exercise}}
\newcommand{\question}{{\bf Question}}
\newcommand{\notation}{{\bf Notation}}
\newcommand{\procedure}{{\bf Procedure}}
\newcommand{\lemma}{{\bf Lemma}}
\newcommand{\thus}{$\Rightarrow$}

\newcommand{\eg}{{\it e.g.}}
\newcommand{\ie}{{\it i.e.}}
\newcommand{\etc}{{\it etc.}}

\newcommand{\threesat}{{\sc 3SAT}}

\renewcommand{\emph}[1]{{\bf #1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Programming Language (essentially ocaml)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\mlkwd}[1]{\mbox{\tt #1}}
\newcommand{\mllet}{\mlkwd{let}}
\newcommand{\mlrec}{\mlkwd{rec}}
\newcommand{\mland}{\mlkwd{and}}
\newcommand{\mlin}{\mlkwd{in}}
\newcommand{\mlraise}{\mlkwd{raise}}
\newcommand{\mlif}{\mlkwd{if}}
\newcommand{\mlthen}{\mlkwd{then}}
\newcommand{\mlelse}{\mlkwd{else}}
\newcommand{\mlband}{\mlkwd{\&\&}}
\newcommand{\mlbor}{\mlkwd{||}}
\newcommand{\mlbnot}{\mlkwd{not}}
\newcommand{\mlignore}{\mlkwd{ignore}}
\newcommand{\mlref}{\mlkwd{ref}}
\newcommand{\mlfalse}{\mlkwd{false}}
\newcommand{\mltrue}{\mlkwd{true}}
\newcommand{\mlassign}{\mlkwd{:=}}
\newcommand{\mlset}{\mlkwd{<-}}
\newcommand{\mlvar}[1]{\memph{#1}}
\newcommand{\mlfn}[1]{\mbox{\sc #1}}
\newcommand{\mltype}[1]{\mbox{\bf #1}}
\newcommand{\mlcons}[1]{\mbox{#1}}
\newcommand{\mlfield}[1]{\mbox{\tt #1}}
\newcommand{\mlmodule}[1]{\mbox{\tt #1}}
\newcommand{\mlcomment}[1]{\mbox{\tt (* #1 *)}}
\newcommand{\mlexception}[1]{\mbox{\bf #1}}

\newcommand{\mlblank}{\underline{\hspace{1em}}}

\newcommand{\mlindent}{\hspace{1em}}
\newcommand{\mlblock}[1]{
  \begin{array}[t]{@{}l}
  #1
  \end{array}
}
\newcommand{\mlconstype}[2]{
  \mlblock{
  \mlkwd{type}\ #1\ = \\
  \begin{array}{@{|\hspace{.5em}}l@{\hspace{1em}\mlkwd{of}\hspace{1em}}l}
  #2
  \end{array}
  }
}
\newcommand{\mlrecordtype}[2]{
  \mlblock{
  \mlkwd{type}\ #1\ =\ \{ \\
  \mlindent \mlblock{
  \begin{array}{l@{\hspace{1em}\mbox{:}\hspace{1em}}l}
  #2
  \end{array} \\
  \}
  }}
}
\newcommand{\mlmatchbody}[1]{
  \begin{array}{@{|\hspace{.5em}}r@{\hspace{1em}\rightarrow\hspace{1em}}l}
  #1
  \end{array}
}
\newcommand{\mlmatch}[2]{
  \mlblock{
  \mlkwd{match}\ #1\ \mlkwd{with} \\
  \mlmatchbody{#2}
  }
}
\newcommand{\mltry}[2]{
  \mlblock{
  \mlkwd{try}\ #1\ \mlkwd{with} \\
  \mlmatchbody{#2}
  }
}
\newcommand{\mlmatchfunction}[2]{
  \mlblock{
  \mllet\ #1\ =\ \mlkwd{function} \\
  \mlmatchbody{#2}
  }
}
\newcommand{\mlwhile}[2]{
  \mlblock{
  \mlkwd{while}\ #1\ \mlkwd{do} \\
  \mlindent
  \mlblock{#2} \\
  \mlkwd{done}
  }
}
\newcommand{\mlsmalllet}[2]{
  \mllet\ #1\ =\ #2\ \mlin
}
\newcommand{\mlbiglet}[2]{
  \mlblock{
  \mllet\ #1\ = \\
  \mlindent
  \mlblock{#2} \\
  \mlin
  }
}
\newcommand{\mlfunction}[2]{
  \mlblock{
  \mllet\ #1\ = \\
  \mlindent
  \mlblock{#2}
  }
}
\newcommand{\mlbeginend}[1]{
  \mlkwd{begin} \\
  \mlindent
  \mlblock{#1} \\
  \mlkwd{end}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% PI
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\pvc}{$\mathsf{\pi VC}$}
\newcommand{\ppi}{{\sf pi}}

\newcommand{\pipre}{{\sf @pre}}
\newcommand{\pipost}{{\sf @post}}
\newcommand{\piassert}{{\sf @}}
\newcommand{\piwf}{$\downarrow$}

\newcommand{\pityp}[1]{{\tt #1}}
\newcommand{\pistruct}{\pikwd{struct}}
\newcommand{\pifn}[1]{{\sc #1}}
\newcommand{\pifnm}[1]{\mbox{\sc #1}}

\newcommand{\pikwd}[1]{{\tt #1}}
\newcommand{\piif}{\pikwd{if}}
\newcommand{\pielse}{\pikwd{else}}
\newcommand{\piwhile}{\pikwd{while}}
\newcommand{\pibreak}{\pikwd{break}}
\newcommand{\picontinue}{\pikwd{continue}}
\newcommand{\pifor}{\pikwd{for}}
\newcommand{\pireturn}{\pikwd{return}}
\newcommand{\pinew}{\pikwd{new}}

\newcommand{\pidiv}{\pikwd{div}}

\newcommand{\pirv}{\mathsf{rv}}

\newcommand{\piblock}[1]{
$\{$ \\ \hspace{1em}\begin{tabular}{@{}l@{}}#1\end{tabular} \\ $\}$
}
\newcommand{\pisblock}[1]{
\\ \hspace{1em}\begin{tabular}{@{}l@{}}#1\end{tabular}
}

\newcommand{\btrue}{\top}
\newcommand{\bfalse}{\bot}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Basic Math and Logic
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\true}{\top}
\newcommand{\false}{\bot}
\newcommand{\truev}{\mbox{\emph{true}}}
\newcommand{\falsev}{\mbox{\emph{false}}}

\newcommand{\set}[1]{\{#1\}}
\newcommand{\largeset}[1]{\left\{#1\right\}}
\newcommand{\range}[2]{\set{#1,\ldots,#2}}
\newcommand{\tuple}[1]{\langle #1 \rangle}
\newcommand{\Tuple}[1]{\left\langle #1 \right\rangle}
\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\eqdef}{\stackrel{\mbox{\scriptsize def}}{=}}

\newcommand{\bimplies}{\rightarrow}
\newcommand{\bequiv}{\leftrightarrow}
\newcommand{\lneg}[1]{\overline{#1}}

\newcommand{\sentence}{{\cal S}}
\newcommand{\sublbl}[2]{#1_{\mbox{\footnotesize\sc #2}}}
\newcommand{\cnfsentence}{\sublbl{\cal S}{cnf}}
\newcommand{\nnfsentence}{\sublbl{\cal S}{nnf}}

\newcommand{\vars}{{\cal V}}
\newcommand{\varss}{\mathsf{vars}}
\newcommand{\tmps}{{\cal U}}
\newcommand{\isvar}[1]{#1 \in \vars}

\newcommand{\vv}[1]{\overline{#1}}

\newcommand{\defvar}[1]{d_{#1}}

\newcommand{\integers}{\mathbb{Z}}
\newcommand{\naturals}{\mathbb{N}}
\newcommand{\rationals}{\mathbb{Q}}
\newcommand{\reals}{\mathbb{R}}
\newcommand{\equality}{\mathbb{E}}
\newcommand{\rds}{\mathbb{D}}
\newcommand{\arrays}{\mathsf{A}}
\newcommand{\lists}{\mathbb{L}}

\newcommand{\tequal}{T_\equality}
\newcommand{\trds}{T_\rds}
\newcommand{\lcons}{\mathsf{cons}}
\newcommand{\lcar}{\mathsf{car}}
\newcommand{\lcdr}{\mathsf{cdr}}
\newcommand{\latom}{\mathsf{atom}} %_{\lcons}}

\newcommand{\mmod}{\widehat{\mbox{mod}}}
\newcommand{\ssign}{\mbox{sign}}
\newcommand{\ffloor}[1]{\left\lfloor #1 \right\rfloor}
\newcommand{\moddef}[2]{#1 - #2\ffloor{\frac{#1}{#2} + \frac{1}{2}}}
\newcommand{\pmoddef}[2]{\left(\moddef{#1}{#2}\right)}

\newcommand{\assl}{{\cal{A}}}
\newcommand{\Tau}{{\cal{T}}}
\newcommand{\locals}{{\cal{L}}}
\newcommand{\formals}{{\cal{F}}}

\newcommand{\asslv}{\assl(\vars)}
\newcommand{\asslvp}{\assl(\vars \cup \vars')}
\newcommand{\exprl}{{\cal{E}}}
\newcommand{\exprlv}{\exprl(\vars)}

%\newcommand{\transys}{\langle \vars, \Theta, \Omega, \Tau \rangle}
%\newcommand{\initc}{\langle \ell_0, \theta \rangle}
%\newcommand{\finalc}{\langle \ell_f, \omega \rangle}
%\newcommand{\tran}{\langle \ell, \ell', \rho_\tau \rangle}
%\newcommand{\tranm}{\langle \ell, m, \rho_\tau \rangle}
%\newcommand{\locs}[1]{\mathsf{locs}(#1)}
%\newcommand{\pres}[1]{\mathsf{pres}(#1)}
%\newcommand{\presr}{\pres{\ldots}}
%\newcommand{\vc}[3]{\set{#1}\rho_{#2}\set{#3}}
%\newcommand{\vclo}[3]{\set{\mu(#1)}\rho_{#2}\set{\mu(#3)}}
%\newcommand{\vcn}[4]{\set{\mu(#1_{#2})}\rho_{\tau_{#3}}\set{\mu(#1_{#4})}}
%\newcommand{\vcl}[3]{\vcn{\ell}{#1}{#2}{#3}}
%\newcommand{\vcm}[3]{\vcn{m}{#1}{#2}{#3}}

\newcommand{\Implies}[2]{#1\ \Rightarrow\ #2}

\newcommand{\subst}{\mathsf{s}}
\newcommand{\isubst}{\mathsf{s}^{-1}}

\newcommand{\tr}[1]{#1^{\mathsf{T}}}
\newenvironment{mymatrix}[1]{\left[\begin{array}{@{}#1@{}}}{\end{array}\right]}
\newenvironment{myvector}{\begin{mymatrix}{c}}{\end{mymatrix}}
\newcommand{\nullsp}[1]{\mathsf{null}(#1)}
\newcommand{\solnsp}[2]{\mathsf{soln}(#1,#2)}
\newcommand{\linsp}[1]{\mathsf{lin}(#1)}
\newcommand{\affsp}[1]{\mathsf{aff}(#1)}
\newcommand{\minc}[2]{\mathsf{minc}(#1, #2)}
\newcommand{\minv}[1]{\mathsf{minv}(#1)}
\newcommand{\vrep}[2]{\mathsf{c2v}(#1, #2)}
\newcommand{\crep}[1]{\mathsf{v2c}(#1)}
\newcommand{\sem}[1]{[\hspace*{-.1em}[#1]\hspace*{-.1em}]}
\newcommand{\apost}[2]{\mathsf{post}(#1,\ #2)}

\newcommand{\pmem}{{\tt mem}}
\newcommand{\pk}[1]{{\tt #1}}

\newcommand{\wpre}[2]{{\sf wpre}(\pk{#1}, \pk{#2})}
\newcommand{\wprem}[2]{\mathsf{wpre}(#1, #2)}
\newcommand{\subs}[1]{$\{$#1$\}$}
\newcommand{\submt}{$\mapsto$~}
\newcommand{\subar}{$\triangleright$~}

\newcommand{\sub}{~/~}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Functions and Predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\awt}[3]{#1 \{ #2 \triangleleft #3 \} }
\newcommand{\ard}[2]{#1[#2]}

\newcommand{\peq}{\mathsf{eq}}
\newcommand{\pbeq}{\mathsf{beq}}
\newcommand{\psort}{\mathsf{sorted}}
\newcommand{\ppart}{\mathsf{partitioned}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Software
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ocaml}{{\sc O'Caml}}
\newcommand{\chaff}{{\sc Chaff}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Algorithms
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% -------------- BubbleSort ------------------------ %

\newcommand{\bbsort}{{\sc BubbleSort}}

\newcommand{\bbsortexpl}{
$
\begin{array}{@{}cccccc@{}}
3 & 4 & 1 & 2 & \rnode{51}{5} & \rnode{61}{6} \\
j &   &   & i &   &   \\ \\
3 & \circlenode{42}{4} & \circlenode{12}{1} & 2 & \rnode{52}{5} & \rnode{62}{6} \\
  & j &   & i &   &   \\ \\
3 & 1 & \circlenode{43}{4} & \circlenode{23}{2} & \rnode{53}{5} & \rnode{63}{6} \\
  &   & j & i &   &   \\ \\
3 & 1 & 2 & 4 & \rnode{54}{5} & \rnode{64}{6} \\
  &   &   & j,i &   &   \\ \\
3 & 1 & 2 & \rnode{45}{4} & 5 & \rnode{65}{6} \\
j &   & i &   &   & 

\ncbox[nodesep=.15,boxsize=.3,linearc=.2,linestyle=dotted]{51}{61}
\ncbox[nodesep=.15,boxsize=.3,linearc=.2,linestyle=dotted]{52}{62}
\ncbox[nodesep=.15,boxsize=.3,linearc=.2,linestyle=dotted]{53}{63}
\ncbox[nodesep=.15,boxsize=.3,linearc=.2,linestyle=dotted]{54}{64}
\ncbox[nodesep=.15,boxsize=.3,linearc=.2,linestyle=dotted]{45}{65}

\ncarc[arcangle=45]{<->}{42}{12}
\ncarc[arcangle=45]{<->}{43}{23}

\end{array}
$
}

\newcommand{\bbsortpcode}{
\begin{tabular}{@{}l@{}}
  \pityp{int[]}\ \pifn{BubbleSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pityp{int}\ $i$, $j$, $t$; \\
    \pifor\ ($i$ := $|a| - 1$; $i > 0$; $i$ := $i - 1$)
    \piblock{
      \pifor\ ($j$ := $0$; $j < i$; $j$ := $j + 1$)
      \piblock{
	\piif\ $(a[j] > a[j + 1])$ 
	\piblock{
	  $t$ := $a[j]$; \\
	  $a[j]$ := $a[j + 1]$; \\
	  $a[j + 1]$ := $t$;
	} \\
      } \\
    } \\
    \pireturn\ $a$;
  }
\end{tabular}
}
\newcommand{\bbsortplcode}{
\begin{tabular}{@{}l@{}}
  \pityp{int[]}\ \pifn{BubbleSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pityp{int}\ $i$, $j$, $t$; \\
    \pifor\ ($i$ := $|a| - 1$; $\ell_1$: $i > 0$; $i$ := $i - 1$)
    \piblock{
      \pifor\ ($j$ := $0$; $\ell_2$: $j < i$; $j$ := $j + 1$)
      \piblock{
	\piif\ $(a[j] > a[j + 1])$ 
	\piblock{
	  $t$ := $a[j]$; \\
	  $a[j]$ := $a[j + 1]$; \\
	  $a[j + 1]$ := $t$;
	} \\
      } \\
    } \\
    \pireturn\ $a$;
  }
\end{tabular}
}

\newcommand{\bbsortcode}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0$ \\
  $\ell_f$: \pipost\ $\psort(\pirv, 0, |a| - 1)$ \\
  \pityp{int[]}\ \pifn{BubbleSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pityp{int}\ $i$, $j$, $t$; \\
    \pifor\ ($i$ := $|a| - 1$; $i > 0$; $i$ := $i - 1$)
    \piblock{
      \pifor\ ($j$ := $0$; $j < i$; $j$ := $j + 1$)
      \piblock{
	\piif\ $(a[j] > a[j + 1])$ 
	\piblock{
	  $t$ := $a[j]$; \\
	  $a[j]$ := $a[j + 1]$; \\
	  $a[j + 1]$ := $t$;
	} \\
      } \\
    } \\
    \pireturn\ $a$;
  }
\end{tabular}
}
\newcommand{\bbsortcodeA}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0$ \\
  $\ell_f$: \pipost\ $\psort(\pirv, 0, |a| - 1)$ \\
  \pityp{int[]}\ \pifn{BubbleSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pityp{int}\ $i$, $j$, $t$; \\
    \pifor\ ($i$ := $|a| - 1$; \fbox{$\ell_1$}: $i > 0$; $i$ := $i - 1$)
    \piblock{
      \pifor\ ($j$ := $0$; \fbox{$\ell_2$}: $j < i$; $j$ := $j + 1$)
      \piblock{
	\piif\ $(a[j] > a[j + 1])$ 
	\piblock{
	  $t$ := $a[j]$; \\
	  $a[j]$ := $a[j + 1]$; \\
	  $a[j + 1]$ := $t$;
	} \\
      } \\
    } \\
    \pireturn\ $a$;
  }
\end{tabular}
}
\newcommand{\bbsortcodeB}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0$ \hfill precondition \\
  $\ell_f$: \pipost\ $\psort(\pirv, 0, |a| - 1)$ \hspace*{10em} postcondition \\
  \pityp{int[]}\ \pifn{BubbleSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pityp{int}\ $i$, $j$, $t$; \\
    \pifor\ ($i$ := $|a| - 1$; $i > 0$; $i$ := $i - 1$)
    \piblock{
      \pifor\ ($j$ := $0$; $j < i$; $j$ := $j + 1$)
      \piblock{
	\piif\ $(a[j] > a[j + 1])$ 
	\piblock{
	  $t$ := $a[j]$; \\
	  $a[j]$ := $a[j + 1]$; \\
	  $a[j + 1]$ := $t$;
	} \\
      } \\
    } \\
    \pireturn\ $a$;
  }
\end{tabular}
}

\newcommand{\bbsortacode}{
\begin{tabular}{@{}l@{}}
  \pipre\ $|a| \ge 0$ \\
  \pipost\ $\psort(\pirv, 0, |a| - 1)$ \\
  \pityp{int[]}\ \pifn{BubbleSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pityp{int}\ $i$, $j$, $t$; \\
    \pifor\
    \piassert 
    $\left[\begin{array}{@{}l@{}}
	-1 \le i < |a|\ \wedge\ |a| = |a|_0 \\
	\wedge\ \ppart(a, 0, i, i+1, |a|-1)\
	\wedge\ \psort(a, i, |a|-1)
      \end{array}\right]$ \\
    ($i$ := $|a| - 1$; $i > 0$; $i$ := $i - 1$)
    \pisblock{
      \pifor\
      \piassert 
      $\left[\begin{array}{@{}l@{}}
	  1 \le i < |a|\ \wedge\ 0 \le j \le i\ \wedge\ |a| = |a|_0 \\
	  \wedge\ \ppart(a, 0, i, i+1, |a|-1) \\
	  \wedge\ \ppart(a, 0, j-1, j, j)\
	  \wedge\ \psort(a, i, |a|-1)
	\end{array}\right]$ \\      
      ($j$ := $0$; $j < i$; $j$ := $j + 1$)
      \pisblock{
	\piif\ $(a[j] > a[j + 1])$ 
	\piblock{
	  $t$ := $a[j]$;\
	  $a[j]$ := $a[j + 1]$;\
	  $a[j + 1]$ := $t$;
	}
      }
    } \\
    \pireturn\ $a$;
  }
\end{tabular}
}
\newcommand{\bbsortacodeA}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0$ \hfill input specification \\
  $\ell_f$: \pipost\ $\psort(\pirv, 0, |a| - 1)$ \hfill output specification \\
  \pityp{int[]}\ \pifn{BubbleSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pityp{int}\ $i$, $j$, $t$; \hfill \rnode{la}{loop assertions} \\
    \pifor\ \rnode{1f}{$\ell_1$}: 
    \piassert 
    $\left[\begin{array}{@{}l@{}}
	-1 \le i < |a|\ \wedge\ |a| = |a|_0 ~~~~ \rnode{0}{} \\
	\wedge\ \ppart(a, 0, i, i+1, |a|-1)\
	\wedge\ \psort(a, i, |a|-1)
      \end{array}\right]$ \\
    ($i$ := $|a| - 1$; \rnode{1t}{}$i > 0$; $i$ := $i - 1$)
    \pisblock{
      \pifor\ \rnode{2f}{$\ell_2$}:
      \piassert 
      $\left[\begin{array}{@{}l@{}}
	  1 \le i < |a|\ \wedge\ 0 \le j \le i\ \wedge\ |a| = |a|_0 
	  ~\rnode{1}{} \\
	  \wedge\ \ppart(a, 0, i, i+1, |a|-1) \\
	  \wedge\ \ppart(a, 0, j-1, j, j)\
	  \wedge\ \psort(a, i, |a|-1)
	\end{array}\right]$ \\      
      ($j$ := $0$; \rnode{2t}{}$j < i$; $j$ := $j + 1$)
      \pisblock{
	\piif\ $(a[j] > a[j + 1])$ 
	\piblock{
	  $t$ := $a[j]$;\
	  $a[j]$ := $a[j + 1]$;\
	  $a[j + 1]$ := $t$;
	}
      }
    } \\
    \pireturn\ $a$;
  }
  \ncline{->}{la}{0}
  \ncarc[arcangle=40]{->}{la}{1}
  \ncarc[arcangle=10]{->}{1f}{1t}
  \ncline{->}{2f}{2t}
\end{tabular}
}

\newcommand{\bbsortcfgplain}{
\begin{tabular}{ccc}
& \circlenode{0}{$\ell_0$} \\
\\
& \circlenode{1}{$\ell_1$} \\
\\
\circlenode{f}{$\ell_f$} && 
\circlenode{2}{$\ell_2$}

\ncline{->}{0}{1}
\ncarc[arcangle=45]{->}{1}{2}
\ncarc[arcangle=-45]{->}{1}{f}
\ncarc[arcangle=45]{->}{2}{1}
\nccircle[angleA=180]{->}{2}{.5}
\end{tabular}
}
\newcommand{\bbsortcfg}{
\begin{tabular}{ccc}
& \circlenode{0}{$\ell_0$} \\
\\
& \circlenode{1}{$\ell_1$} \\
\\
\circlenode{f}{$\ell_f$} && 
\circlenode{2}{$\ell_2$}

\ncline{->}{0}{1}
\trput{$\pi_0$}
\ncarc[arcangle=45]{->}{1}{2}
\trput{$\pi_1^T$}
\ncarc[arcangle=-45]{->}{1}{f}
\tlput{$\pi_1^F$}
\ncarc[arcangle=45]{->}{2}{1}
\tlput{$\pi_2^3$}
\nccircle[angleA=180]{->}{2}{.5}
\tbput{$\pi_2^1, \pi_2^2$}
\end{tabular}
}

\newcommand{\bbsorttcode}{
\begin{tabular}{@{}l@{}}
  \pipre\ $|a| \ge 0$ \\
  \pipost\ $\truev$ \\
  \pityp{int[]}\ \pifn{BubbleSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pityp{int}\ $i$, $j$, $t$; \\
    $\ell_1$: \pifor \\
    \hspace*{2em}\piassert\ $(i + 1 \ge 0)$\ \piwf\ $(i+1, i, 1)$ \\
    \hspace*{2em}($i$ := $|a| - 1$; $i > 0$; $i$ := $i - 1$)
    \pisblock{
      $\ell_2$: \pifor \\ 
      \hspace*{2em}\piassert\ $(i - j \ge 0)$\ \piwf\ $(i+1, i-j, 0)$ \\
      \hspace*{2em}($j$ := $0$; $j < i$; $j$ := $j + 1$)
      \pisblock{
	\piif\ $(a[j] > a[j + 1])$ 
	\piblock{
	  $t$ := $a[j]$;\
	  $a[j]$ := $a[j + 1]$;\
	  $a[j + 1]$ := $t$;
	}
      }
    } \\
    \pireturn\ $a$;
  }
\end{tabular}
}

% --------------- MergeSearch ---------------------- %

\newcommand{\msort}{{\sc MergeSort}}
\newcommand{\msortcode}{
\begin{tabular}{@{}l@{}}
  \pipre\ $|a| \ge 0$ \\
  \pipost\ $\psort(\pirv, 0, |\pirv| - 1)$ \\
  \pityp{int[]}\ \pifn{MergeSort}(\pityp{int[]}\ $a$)
  \piblock{
    \pireturn\ \pifn{ms}$(a, 0, |a| - 1)$;
  } \\
  \\

  \pipre\ $0 \le \ell\ \wedge\ u < |a|$ \\
  \pipost\ $\left[\begin{array}{ll}
      & \psort(l, u, \pirv)\ \wedge\ |\pirv| = |a| \\
      \wedge & \pbeq(0, \ell - 1, \pirv, a)\
      \wedge\ \pbeq(u + 1, |a| - 1, \pirv, a)
    \end{array}\right]$ \\
  \pityp{int[]}\ \pifn{ms}(\pityp{int[]}\ $a$, \pityp{int}\ $\ell$, \pityp{int}\ $u$);
\end{tabular}
}

% --------------- BinarySearch --------------------- %

\newcommand{\bsearch}{{\sc BinarySearch}}
\newcommand{\bsearchcodea}{
\begin{tabular}{@{}l@{}}
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$;
  }
\end{tabular}
}
\newcommand{\bsearchcodeb}{
\begin{tabular}{@{}l@{}}
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \\
      \pielse\ \piif\ $(a[m] < e)$ \pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \\
      \pielse\ \pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
    }
  }
\end{tabular}
}

\newcommand{\bsearchacodea}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $\ell_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[0 \le i < |a|\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$;
  }
\end{tabular}
}
\newcommand{\bsearchacodeaB}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $\ell_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[0 \le i < |a|\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$; \hspace*{9em} $\ldots\pi_0$
  }
\end{tabular}
}
\newcommand{\bsearchacodeb}{
\begin{tabular}{@{}l@{}}
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \\
      \pielse\ \piif\ $(a[m] < e)$ \pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \\
      \pielse\ \pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
    }
  }
\end{tabular}
}
\newcommand{\bsearchacodebA}{
\begin{tabular}{@{}l@{}}
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \hfill $\ldots \pi_1$ \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \hfill $\ldots \pi_2$ \\
      \pielse\ \piif\ $(a[m] < e)$ \pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \hspace*{1em} $\ldots\pi_3$ \\
      \pielse\ \pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$; \hfill $\ldots\pi_4$
    }
  }
\end{tabular}
}
\newcommand{\bsearchacodebB}{
\begin{tabular}{@{}l@{}}
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ \underline{$(\ell > u)$} \pireturn\ $\falsev$; \\
    \underline{\pielse}\ \piblock{
      \underline{$m$ := $(\ell + u)$ \pidiv\ $2$;} \\
      \underline{\piif\ $(a[m] = e)$\ \pireturn\ $\truev$;} \hspace*{12em} $\ldots\pi_2$ \\
      \pielse\ \piif\ $(a[m] < e)$ \pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \\
      \pielse\ \pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
    }
  }
\end{tabular}
}
\newcommand{\bsearchacodeaA}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0\ \wedge\ \psort(a, 0, |a| - 1)$ \hfill precondition \\
  $\ell_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[0 \le i < |a|\ \wedge\ a[i] = e]$ \hspace*{2em} postcondition \\
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$;
  }
\end{tabular}
}
\newcommand{\bsearchacodebC}{
\begin{tabular}{@{}l@{}}
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \hspace*{3em} precondition \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \hfill postcondition \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \\
      \pielse\ \piif\ $(a[m] < e)$ \pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \\
      \pielse\ \pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
    }
  }
\end{tabular}
}
\newcommand{\bsearchacodeA}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0\ \wedge\ \psort(a, 0, |a| - 1)$ \hfill precondition \\
  $\ell_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[0 \le i < |a|\ \wedge\ a[i] = e]$ \hfill postcondition \\
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$;
  } \\
  \\
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \hspace*{3em} precondition \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \hfill postcondition \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \\
      \pielse\ \piif\ $(a[m] < e)$ \pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \\
      \pielse\ \pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
    }
  }
\end{tabular}
}

\newcommand{\bsearchcfga}{
\begin{tabular}{c}
  \circlenode{l0}{$\ell_0$}
  \\ \\
  \circlenode{lf}{$\ell_f$}

  \ncline{->}{l0}{lf}
  \trput{$\pi_0$}
\end{tabular}
}
\newcommand{\bsearchcfgb}{
\begin{tabular}{c}
  \circlenode{m0}{$m_0$}
  \\ \\
  \circlenode{mf}{$m_f$}

  \ncline{->}{m0}{mf}
  \trput{$\pi_1,\pi_2,\pi_3,\pi_4$}
\end{tabular}
}

\newcommand{\bsearchargcodeb}{
\begin{tabular}{@{}l@{}}
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \\
      \pielse\ \piif\ $(a[m] < e)$ \piblock{
	$m_1$: \piassert\ $0 \le m+1\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a|-1)$; \\
	\pireturn\ \pifn{BSearch}$(a, m+1, u, e)$;
      } \\
      \pielse\ \piblock{
	$m_2$: \piassert\ $0 \le \ell\ \wedge\ m-1 < |a|\ \wedge\ \psort(a, 0, |a|-1)$; \\
	\pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
      }
    }
  }
\end{tabular}
}
\newcommand{\bsearchargcodebA}{
\begin{tabular}{@{}l@{}}
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \hfill $\ldots\pi_1$ \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \hfill $\ldots\pi_2$ \\
      \pielse\ \piif\ $(a[m] < e)$ \piblock{
	$m_1$: \piassert\ $0 \le m+1\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a|-1)$; \hspace*{1.1em}$\ldots\pi_3^a$ \\
	\pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \hfill $\ldots\pi_3$
      } \\
      \pielse\ \piblock{
	$m_2$: \piassert\ $0 \le \ell\ \wedge\ m-1 < |a|\ \wedge\ \psort(a, 0, |a|-1)$; \hspace*{1.1em} $\ldots\pi_4^a$ \\
	\pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$; \hfill $\ldots\pi_4$
      }
    }
  }
\end{tabular}
}
\newcommand{\bsearchrgcfgb}{
\begin{tabular}{@{\hspace{5em}}ccc}
  \circlenode{m0}{$m_0$}
  \\ \\
  & \dianode{m1}{$m_1$} & \dianode{m2}{$m_2$} 
  \\ \\
  \circlenode{mf}{$m_f$}

  \ncline{->}{m0}{mf}
  \tlput{$\pi_1,\pi_2,\pi_3,\pi_4$}
  \ncline{->}{m0}{m1}
  \trput{$\pi_3^a$}
  \ncarc[arcangle=20]{->}{m0}{m2}
  \trput{$\pi_4^a$}
  \ncline[linestyle=dotted]{->}{m1}{mf}
  \ncline[linestyle=dotted]{->}{m2}{mf}
\end{tabular}
}

\newcommand{\bsearchagcodea}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $\ell_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[0 \le i < |a|\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    $\ell_1$: \piassert\ $0 \le 0\ \wedge\ |a| - 1 < |a|\ \wedge\ \psort(a, 0, |a| - 1)$; \\
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$;
  }
\end{tabular}
}
\newcommand{\bsearchagcodeaA}{
\begin{tabular}{@{}l@{}}
  $\ell_0$: \pipre\ $|a| \ge 0\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $\ell_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[0 \le i < |a|\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    $\ell_1$: \piassert\ $0 \le 0\ \wedge\ |a| - 1 < |a|\ \wedge\ \psort(a, 0, |a| - 1)$; \hspace*{2em} $\ldots\pi_0^a$ \\
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$; \hfill $\ldots\pi_0$
  }
\end{tabular}
}
\newcommand{\bsearchagcodeb}{
\begin{tabular}{@{}l@{}}
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \\
    \pielse\ \piblock{
      $m_1$: \piassert\ $2 \ne 0$; \\
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      $m_2$: \piassert\ $0 \le m < |a|$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \\
      $m_3$: \piassert\ $0 \le m < |a|$; \\
      \pielse\ \piif\ $(a[m] < e)$ \piblock{
	$m_4$: \piassert\ $0 \le m+1\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a|-1)$; \\
	\pireturn\ \pifn{BSearch}$(a, m+1, u, e)$;
      } \\
      \pielse\ \piblock{
	$m_5$: \piassert\ $0 \le \ell\ \wedge\ m-1 < |a|\ \wedge\ \psort(a, 0, |a|-1)$; \\
	\pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
      }
    }
  }
\end{tabular}
}
\newcommand{\bsearchagcodebA}{
\begin{tabular}{@{}l@{}}
  $m_0$: \pipre\ $0 \le \ell\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a| - 1)$ \\
  $m_f$: \pipost\ $\pirv\ \leftrightarrow\ (\exists i)[\ell \le i \le u\ \wedge\ a[i] = e]$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \hfill $\ldots\pi_1$ \\
    \pielse\ \piblock{
      $m_1$: \piassert\ $2 \ne 0$; \hfill $\ldots\pi_1^b$ \\
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      $m_2$: \piassert\ $0 \le m < |a|$; \hfill $\ldots\pi_2^b$ \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \hfill $\ldots\pi_2$ \\
      $m_3$: \piassert\ $0 \le m < |a|$; \hfill $\ldots\pi_3^b$ \\
      \pielse\ \piif\ $(a[m] < e)$ \piblock{
	$m_4$: \piassert\ $0 \le m+1\ \wedge\ u < |a|\ \wedge\ \psort(a, 0, |a|-1)$; \hspace*{1.1em} $\ldots\pi_3^a$ \\
	\pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \hfill $\ldots\pi_3$
      } \\
      \pielse\ \piblock{
	$m_5$: \piassert\ $0 \le \ell\ \wedge\ m-1 < |a|\ \wedge\ \psort(a, 0, |a|-1)$; \hspace*{1.2em} $\ldots\pi_4^a$ \\
	\pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$; \hfill $\ldots\pi_4$
      }
    }
  }
\end{tabular}
}

\newcommand{\bsearchgcfga}{
\begin{tabular}{@{\hspace{2em}}c}
  \circlenode{l0}{$\ell_0$}
  \\ \\
  \dianode{l1}{$\ell_1$}
  \\ \\
  \circlenode{lf}{$\ell_f$}

  \ncline{->}{l0}{l1}
  \trput{$\pi_0^a$}
  \ncline[linestyle=dotted]{->}{l1}{lf}
  \ncarc[arcangle=-45]{->}{l0}{lf}
  \tlput{$\pi_0$}
\end{tabular}
}
\newcommand{\bsearchgcfgb}{
\begin{tabular}{@{\hspace{4em}}c@{}ccccc}
  \circlenode{m0}{$m_0$} \\
  \\
  &
  \dianode{m1}{$m_1$} &
  \dianode{m2}{$m_2$} &
  \dianode{m3}{$m_3$} &
  \dianode{m4}{$m_4$} &
  \dianode{m5}{$m_5$} \\
  \\
  \circlenode{mf}{$m_f$}

  \ncline{->}{m0}{m1}
  \trput{$\pi_1^b$}
  \ncline{->}{m0}{m2}
  \trput{$\pi_2^b$}
  \ncarc[arcangle=15]{->}{m0}{m3}
  \trput{$\pi_3^b$}
  \ncarc[arcangle=20]{->}{m0}{m4}
  \trput{$\pi_3^a$}
  \ncarc[arcangle=20]{->}{m0}{m5}
  \trput{$\pi_4^a$}
  \ncline[linestyle=dotted]{->}{m1}{mf}
  \ncline[linestyle=dotted]{->}{m2}{mf}
  \ncline[linestyle=dotted]{->}{m3}{mf}
  \ncarc[arcangle=15,linestyle=dotted]{->}{m4}{mf}
  \ncarc[arcangle=15,linestyle=dotted]{->}{m5}{mf}
  \ncline{->}{m0}{mf}
  \tlput{$\pi_1,\pi_2,\pi_3,\pi_4$}
\end{tabular}
}

\newcommand{\bsearchtcodea}{
\begin{tabular}{@{}l@{}}
  \pipre\ $|a| \ge 0$ \\
  \pipost\ $\truev$ \\
  \piwf\ $(1,0)$ \\
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$;
  }
\end{tabular}
}
\newcommand{\bsearchtcodeb}{
\begin{tabular}{@{}l@{}}
  \pipre\ $u - \ell + 1 \ge 0$ \\
  \pipost\ $\truev$ \\
  \piwf\ $(0,u - \ell + 1)$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \\
      \pielse\ \piif\ $(a[m] < e)$ \pireturn\ \pifn{BSearch}$(a, m+1, u, e)$; \\
      \pielse\ \pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
    }
  }
\end{tabular}
}

\newcommand{\bsearchgtcodea}{
\begin{tabular}{@{}l@{}}
  \pipre\ $|a| \ge 0$ \\
  \pipost\ $\truev$ \\
  \piwf\ $(1,0)$ \\
  \pityp{bool}\ \pifn{BinarySearch}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    $\ell_1$: \piassert\ $(|a|-1) - 0 + 1 \ge 0$ \\
    ~~~~ \piwf\ $(0,(|a|-1) - 0 + 1)$; \\
    \pireturn\ \pifn{BSearch}$(a, 0, |a| - 1, e)$;
  }
\end{tabular}
}
\newcommand{\bsearchgtcodeb}{
\begin{tabular}{@{}l@{}}
  \pipre\ $u - \ell + 1 \ge 0$ \\
  \pipost\ $\truev$ \\
  \piwf\ $(0,u - \ell + 1)$ \\
  \pityp{bool}\ \pifn{BSearch}(\pityp{int[]}\ $a$, \pityp{int} $\ell$, \pityp{int} $u$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $m$; \\
    \piif\ $(\ell > u)$ \pireturn\ $\falsev$; \\
    \pielse\ \piblock{
      $m$ := $(\ell + u)$ \pidiv\ $2$; \\
      \piif\ $(a[m] = e)$\ \pireturn\ $\truev$; \\
      \pielse\ \piif\ $(a[m] < e)$ \piblock{
	$m_1$: \piassert\ $u - (m+1) + 1 \ge 0$ \\
	~~~~~ \piwf\ $(0, u - (m+1) + 1)$; \\
	\pireturn\ \pifn{BSearch}$(a, m+1, u, e)$;
      } \\
      \pielse\ \piblock{
	$m_2$: \piassert\ $(m-1) - \ell + 1 \ge 0$ \\
	~~~~~ \piwf\ $(0, (m-1) - \ell + 1)$; \\
	\pireturn\ \pifn{BSearch}$(a, \ell, m-1, e)$;
      }
    }
  }
\end{tabular}
}

% -------------------- Search ---------------------- %

\newcommand{\psearch}{{\sc Search}}
\newcommand{\psearchcode}{
\begin{tabular}{@{}l@{}}
  \pityp{bool}\ \pifn{Search}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $i$; \\
    \pifor\ ($i$ := 0; $i < |a|$; $i$ := $i + 1$)
    \pisblock{
      \piif\ ($a[i] = e$)\ \pireturn\ $\truev$;
    } \\
    \pireturn\ $\falsev$;
  }
\end{tabular}
}
\newcommand{\psearchscode}{
\begin{tabular}{@{}l@{}}
  \pipre\ $\truev$ \\
  \pipost\ $\pirv\ \leftrightarrow\ (\exists i \in [0,|a|-1])[a[i] = e]$ \\
  \pityp{bool}\ \pifn{Search}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $i$; \\
    \pifor\ ($i$ := 0; $i < |a|$; $i$ := $i + 1$)
    \pisblock{
      \piif\ ($a[i] = e$)\ \pireturn\ $\truev$;
    } \\
    \pireturn\ $\falsev$;
  }
\end{tabular}
}
\newcommand{\psearchniacode}{
\begin{tabular}{@{}l@{}}
  \pipre\ $\truev$ \\
  \pipost\ $\pirv\ \leftrightarrow\ (\exists i \in [0,|a|-1])[a[i] = e]$ \\
  \pityp{bool}\ \pifn{Search}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $i$; \\
    \pifor\ 
    \piassert\
    $0 \le i \le |a|\ \wedge\ (\forall i \in [0,i-1])[a[i] \ne e]$ \\
    ($i$ := 0; $i < |a|$; $i$ := $i + 1$)
    \pisblock{
      \piif\ ($a[i] = e$)\ \pireturn\ $\truev$;
    } \\
    \pireturn\ $\falsev$;
  }
\end{tabular}
}
\newcommand{\psearchacode}{
\begin{tabular}{@{}l@{}}
  \pipre\ $\truev$ \\
  \pipost\ $\pirv\ \leftrightarrow\ (\exists i \in [0,|a|-1])[a[i] = e]$ \\
  \pityp{bool}\ \pifn{Search}(\pityp{int[]}\ $a$, \pityp{int}\ $e$)
  \piblock{
    \pityp{int}\ $i$; \\
    \pifor\ 
    \piassert
    $\left[\begin{array}{@{}l@{}}
	0 \le i \le |a| \\
	\wedge\ (\forall i \in [0,i-1])[a[i] \ne e] \\
	\wedge\ |a| = |a_0|\ \wedge\ e = e_0 \\
	\wedge\ \pbeq(0, |a| - 1, a, a_0)
      \end{array}\right]$ \\
    ($i$ := 0; $i < |a|$; $i$ := $i + 1$)
    \pisblock{
      \piif\ ($a[i] = e$)\ \pireturn\ $\truev$;
    } \\
    \pireturn\ $\falsev$;
  }
\end{tabular}
}
