# Typesetting Hoare triples - padding

I'm trying to typeset a Hoare triple, which is used for reasoning about program correctness. In the text I'm referring to, they look something like this:

I'm aware the stmaryrd package includes relevant commands, so I've tried something like this:

\usepackage{stmaryrd}
\usepackage{mathtools}
\DeclarePairedDelimiter\Hoare{\llparenthesis}{\rrparenthesis}
% ...
$\Hoare*{x > 0} P \Hoare*{y \cdot y < x}$


Unfortunately, this gives me a Missing delimiter (. inserted). \Hoare*{x > 0} error. If I remove the asterisk from the command, it compiles but the spacing looks off:

Notice how close the parentheses are to the contents of the pre and post conditions. How should I go about improving this?

• \llparenthesis and \rrparenthesis are not “growing delimiters”: they're only available at a single size. – egreg May 18 '17 at 20:11
• @egreg That's interesting to know, but I thought the growing delimiters simply changed height (which I'm not too fussed about, it's more the space between the contents and the delimiters I want). Are there visually similar commands from another package I could use instead which would qualify as "growing delimiters"? – Adam Williams May 18 '17 at 20:13

The symbols \llparenthesis and \rrparenthesis are not “growing delimiters” and are only available at standard size.

I suggest a different syntax, in order to cope with the spacing of the middle term:

\documentclass{article}
\usepackage{stmaryrd}

\newcommand\Hoaretriple[3]{%
\llparenthesis\,#1\,\rrparenthesis
\mathrel{#2}\nolinebreak
\llparenthesis\,#3\,\rrparenthesis
}

\begin{document}

$\Hoaretriple{x > 0}{ P }{y \cdot y < x}$

\end{document}


• I like having a command to represent and entire Hoare triple, seems more semantic than the original approach. – Adam Williams May 19 '17 at 13:08

You could fix the spacing manually by inserting some command for it. Either by inserting the space in your \Hoare definition like I did or directly in the formula.

\documentclass{article}
\usepackage{stmaryrd}
\usepackage{mathtools}
\DeclarePairedDelimiter\Hoare{\,\llparenthesis\,}{\,\rrparenthesis\,}
\begin{document}
$\Hoare{x > 0} P \Hoare{y \cdot y < x}$
\end{document}


• Thanks for linking that documentation! I was using horrible hacks like \text{ } to try and get around this, before. – Adam Williams May 18 '17 at 20:18