1
$\begingroup$

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?

$\endgroup$
4
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.