# How to get proof rules with pseudo-code in them?

I wish to typeset some deduction rules for Hoare logic as sequents with the pseudo-code using the algorithmic package. I have tried using \frac{}{}, but then e.g. if then else gets flattened. I have also tried bussproofs. Again the pseudo-code was flattened to one line.

What would be a good way to get (with a shorter hline of course)

{ I ∧ B } S { I }

{ I }

while B do
S
od


{ I ∧ ¬ B }

What I've been seeing with my efforts up to now was similar to

{ I ∧ B } S { I }

{ I } while B do Sod { I ∧ ¬ B }

Now, I'm experimenting with putting the bottom Hoare-triple in a minipage.

\documentclass{beamer}
\usepackage{algorithmic}
\usepackage{bussproofs}

\renewcommand{\algorithmicendwhile}{{\bf od}}
\newcommand{\textmath}[1]{\text{\it #1}}

\newenvironment{Condition}{\{\,}{\,\}\;}
\newenvironment{Pseudocode}{\begin{algorithmic}}{\end{algorithmic}}
\newcommand{\hoareTripleMM}[3]{\{\,#1\,\}\;#2\;\{\,#3\,\}}

\begin{document}

\begin{frame}
\begin{prooftree}
\AxiomC{$$\hoareTripleMM{V}{\textmath{init}}{I}$$}
\AxiomC{$$\hoareTripleMM{I \land B}{S}{I}$$}
\AxiomC{$$(I \land \neg B) \implies P$$}
\RightLabel{(W2)}
\TrinaryInfC{
\begin{minipage}{68pt}
$$\begin{Condition} V \end{Condition}$$
\begin{Pseudocode}
\STATE $$\textmath{init}$$
\WHILE{$$B$$} $$S$$ \ENDWHILE
\end{Pseudocode}
$$\begin{Condition} P \end{Condition}$$
\end{minipage}
}
\end{prooftree}
\end{frame}
\end{document}


There are still some issues:

1. There is vertical space between the pre-condition and the pseudo-code that I do not yet know where it comes from.
2. There is a LaTeX error: "Something's wrong--perhaps a missing \item." that only occurs when the Pseudocode clock is in there.
3. I'd like the width of the minipage to be taken from the width of the pseudo-code.

I'd like to use algorithmic if that's possible, since I am already using that package quite a bit.

-
What do you mean with "if then else get flattened"? Could you provide a minimal example of what you have so far, pointing out what is wrong with it? –  JLDiaz Jul 19 '12 at 14:44
The "missing \item" error goes away if you put \STATE in front of $$S$$. It's not clear what output you're expecting. –  egreg Jul 19 '12 at 17:55
@egreg: thanks for the hint. The output is now almost what I wanted, but I didn't want the vertical space between the pre-condition and the pseudo-code. –  Marko Jul 19 '12 at 20:45

An algorithmic environment is just a list, so it's typeset to the current line width. Thus it's not possible to avoid specifying the width of the minipage.

In order to avoid the big space, just add \endgraf after the first element:

\documentclass{article}
\usepackage{algorithmic}
\usepackage{bussproofs}
\usepackage{amsmath}
\usepackage{varwidth}

\renewcommand{\algorithmicendwhile}{{\bf od}}
\newcommand{\textmath}[1]{\text{\it #1}}

\newenvironment{Condition}{\{\,}{\,\}\;}
\newenvironment{Pseudocode}{\algorithmic}{\endalgorithmic}
\newcommand{\hoareTripleMM}[3]{\{\,#1\,\}\;#2\;\{\,#3\,\}}

\begin{document}

\begin{prooftree}
\AxiomC{$$\hoareTripleMM{V}{\textmath{init}}{I}$$}
\AxiomC{$$\hoareTripleMM{I \land B}{S}{I}$$}
\AxiomC{$$(I \land \neg B) \implies P$$}
\RightLabel{(W2)}
\TrinaryInfC{%
\begin{minipage}{68pt}
$$\begin{Condition} V \end{Condition}$$\endgraf
\begin{Pseudocode}
\STATE $$\textmath{init}$$
\WHILE{$$B$$} \STATE $$S$$ \ENDWHILE
\end{Pseudocode}
$$\begin{Condition} P \end{Condition}$$
\end{minipage}%
}
\end{prooftree}
\end{document}


One has to use \endgraf because the \TrinaryInfC macro chokes when \par is in its argument.

-
Looks good! Would it be possible to save the algorithmic environment to a box, trim off whitespace on the right, and then determine the width of the resulting box? –  Marko Jul 20 '12 at 14:46
@Marko Sorry, no: the lines are the whole \linewidth long. It may be possible to dismantle the box and every line in it, getting only the text. For such a tiny bit of text it's simply more convenient to type it directly without algorithmic, I'd say. –  egreg Jul 20 '12 at 15:04