what is the 'x :=' part mean in a hoare triple?

Question

In Hoare logic, there's a thing called a Hoare triple, e.g.$$ \begin{array}{ccccc} \{x = 2\} & & x := x+1 & & \{x = 3\} \end{array}. $$ What does '$x :=$' mean?

Answer 1

Short answer, it's an assignment, but it's not part of Hoare logic.

It means whatever it means in the programming language you're using.

A Hoare triple in general looks like $\{P\}\; C\; \{Q\}$ (stolen from the all-knowing wiki), where:

• $P$ and $Q$ are assertions about the state of the system before and after $C$ is executed; and
• $C$ is some piece of code.

So the meaning of $x :=$ depends entirely on the semantics of the code.

Assuming someone hasn't written this as a trick, $:=$ is usually used as an assignment operator (to avoid confusion with $=$ as equality), so in this case the line should be read as $x := x + 1$, i.e., the line of code is incrementing the variable $x$.

If the triple were written in a C-like language, you could write it as $\{x=2\}\; x=x+1;\; \{x=3\}$, or similarly in your favourite language.