what is the 'x :=' part mean in a hoare triple? - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-08-22T07:27:28Z https://cs.stackexchange.com/feeds/question/87787 http://www.creativecommons.org/licenses/by-sa/3.0/rdf https://cs.stackexchange.com/q/87787 1 what is the 'x :=' part mean in a hoare triple? Tremmer Scott https://cs.stackexchange.com/users/83941 2018-02-07T02:36:42Z 2018-02-07T05:08:00Z <p>In <a href="https://en.wikipedia.org/wiki/Hoare_logic" rel="nofollow noreferrer">Hoare logic</a>, there's a thing called a <a href="https://en.wikipedia.org/wiki/Hoare_logic#Hoare_triple" rel="nofollow noreferrer"><em>Hoare triple</em></a>, e.g.$$\begin{array}{ccccc} \{x = 2\} &amp; &amp; x := x+1 &amp; &amp; \{x = 3\} \end{array}.$$ What does '$x :=$' mean?</p> https://cs.stackexchange.com/questions/87787/-/87790#87790 4 Answer by Luke Mathieson for what is the 'x :=' part mean in a hoare triple? Luke Mathieson https://cs.stackexchange.com/users/1636 2018-02-07T04:27:04Z 2018-02-07T04:27:04Z <p>Short answer, it's an assignment, but it's not part of Hoare logic.</p> <p>It means whatever it means in the programming language you're using.</p> <p>A Hoare triple in general looks like $\{P\}\; C\; \{Q\}$ (stolen from the <a href="https://en.wikipedia.org/wiki/Hoare_logic" rel="nofollow noreferrer">all-knowing wiki</a>), where:</p> <ul> <li>$P$ and $Q$ are assertions about the state of the system before and after $C$ is executed; and</li> <li>$C$ is some piece of code.</li> </ul> <p>So the meaning of $x :=$ depends entirely on the semantics of the code.</p> <p>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$.</p> <p>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.</p>