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

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?

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.

• To be more specific, := is assignment in Algol-derived languages such as Pascal. – reinierpost Feb 7 '18 at 16:51