5

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:

Hoare triple

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:

Attempt 1

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
4

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}

enter image description here

|improve this answer|||||
  • 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
3

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}

enter image description here

|improve this answer|||||
  • 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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.