The Blog of Bob Rubbens

Blog - Academia - Projects - About me

Hoare Triple: Notation Evolution

This is a piece of writing that was supposed to end up in my thesis. 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¹ 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², 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.³

The style switch seems to have been initiated by Susan Owicki in her PhD thesis⁴, 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’’⁵. 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.

View as: md (raw), txt.

Generated with BYOB. License: CC-BY-SA. This page is designed to last.

⇐ [This site is part of the UT webring] ⇒