---
title: "Hoare Triple: Notation Evolution"
author: Bob Rubbens
publish_timestamp: 2025-10-25T23:27:30+02:00
state: published
template: post.mako
id: fdd2b0c7-84a6-4187-98a4-638f4a1c8d60
---

*This is a piece of writing that was supposed to end up in [my thesis](https://doi.org/10.3990/1.9789036569101). Unfortunately, because of ~~the publish or perish dynamic~~ bad planning on my part, the interesting part of the piece fell off the page. Since it's a small and interesting piece of history, I generalized the piece a bit, and republished it here. Enjoy!*

In 1969, C.A.R. Hoare defined the *Hoare triple*[^Hoare69] for reasoning about program correctness. Since then, Hoare triples have deeply taken root in the field of program correctness. For example, have a look at the Concrete Semantics book[^Nipkow2014], where they fully formalize the notion in Isabelle.

These days, researches typically use the following syntax for Hoare triples:

$$
\{ \: P \: \} \: c \: \{ \: Q \: \}
$$

Here, $P$ and $Q$ are first-order logic assertions, such as $x > 1$ or $\textsf{isPrime}(p)$. The constant $c$ represents a program. For example, $\texttt{foo()}$, or $\texttt{x = 3; y = x + 2;}$.  Putting this all together, here's an example of a fully formed Hoare triple:

$$
\{ \: x > 0 \: \} \: x := x + 1 \: \{ \: x > 1 \: \} 
$$

The meaning of a Hoare triple is a bit involved, but it boils down to the following: assuming $P$ holds in some state $s$, if $c$ is executed in that state $s$, after that $Q$ should hold. Naturally, whether this is the case for particular $P$, $c$ and $Q$ depends on what you put in the placeholders. This is the interesting part of Hoare logic: Hoare proposed rules so you can transform and decompose these Hoare triples into smaller parts. Then, if you can prove that the smaller parts are correct, the larger Hoare triple is also correct.
While that's all a bit out of scope for this post, you can imagine such a decomposition and proof exists for the $x > 0$ example above.

Now, on to the main part of this post: Hoare originally actually used slightly different syntax:

$$
P \: \{ \: c \: \} \: Q
$$

The difference being that he put brackets around the program, and not around the pre- and postcondition. To the best of my knowledge, to this day the style with braces around the assertions is more widely used. This also seems to be the consensus in the community, e.g. see Derakhshan et al.[^Derakhshan2023]

The style switch seems to have been initiated by Susan Owicki in her PhD thesis[^Owicki1975], which is the first document that places the braces around the assertions, also to the best of my knowledge. Hoare kept using his original notation, at least until the late 80s.

The reason for changing the notation is not clear. At least one source claims it improves readability, paraphrasing, "especially when reasoning about parallel programs''[^Krzysztof2019]. I don't really understand that line of reasoning, and I also couldn't find an example of this in the paper by Krzysztof et al. All I can say is that, having been "raised" with the brackets-outside notation, I also prefer it over the original notation, even though functionally there doesn't seem to be any difference or limitations.

[^Derakhshan2023]: Hoare triples I & II, by Derakhshan, Farzaneh and Muller, Stefan and Sasaki, Jim and Gordon, Mike. <http://cs.iit.edu/~smuller/cs536-f23/lectures/07-hoaretrp.pdf>

[^Owicki1975]: Axiomatic Proof Techniques for Parallel Programs, by Susan S. Owicki. <https://hdl.handle.net/1813/6393>

[^Krzysztof2019]: Fifty years of Hoare’s logic, by Apt, Krzysztof and Olderog, Ernst-Rüdiger. Section 3.1. <https://doi.org/10.1007/s00165-019-00501-3>

[^Hoare69]: An Axiomatic Basis for Computer Programming, by C.A.R. Hoare. <https://doi.org/10.1145/363235.363259>

[^Nipkow2014]: Concrete Semantics - With Isabelle/HOL, by Tobias Nipkow and Gerwin Klein. <https://doi.org/10.1007/978-3-319-10542-0>