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

Question

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.

Answer 1

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.