Software correctness is a neat way to tie specifications to code implementation. Correctness by construction helps you be absolutely sure your code performs according to specifications. The computer science construct often used for this is Hoare Triples. This Microsoft Research Labs Video has piqued my interest in the practical aspects of Invariants so I thought I’d give a simple overview of Hoare Triples.

Hoare triples are usually written in the format of {P}S{Q} where P is the precondition and Q is the postcondition. Let’s take for example:

` {P} x := y + 1 {x > 5} `

The goal is to find the weakest precondition that creates a correct program.

Using the assignment axiom we substitute the precondition for the postcondtion, pretty simple:

` {x > 5}[x := y + 1] `

Which results in:

` {y + 1 > 5} = {y > 4} `

Therefore our complete listing is now:

` {y > 4} x := y + 1 {x > 5} `

We can deduce that in order for x to be greater than 5 at the end of our listing, y has to be greater than 4 before our code executes.

This is our weakest predicate P. Of course, this is a fairly trivial example, but I hope it gets you started in predicate logic and hoare triple notation. For more information I recommend reading “What Computing is All About”.