If I want to extend a new language by adding a new command havoc x, which updates the variable x with a non-deterministic value, how to write operational semantics rule for havoc x? I'm confused about generate a non-deterministic value. If I write like this: $$\frac{n = [e]_ {intexp}\sigma}{(\mathrm{havoc}\ x,\sigma)\rightarrow(x:=x+n,\sigma)}$$ is it make sense?


I'm going to assume that all the allowed values for $x$ are (unbounded) integers.

In that case your proposal somewhat makes sense, insomuch as $e$ is some arbitrary well-formed expression (which evaluates to some value in the context $\sigma$). But it's just as easy to write this

$$\frac{n\in\mathbb{Z}}{(\mathrm{havoc}\ x,\sigma)\rightarrow (x:=n,\sigma)} $$

You see that in both cases the result of the evaluation by this rule can non-deterministically give any value in $\mathbb{Z}$ to $x$. In this sense, you have a family of rules, one for each $n\in\mathbb{Z}$.

| cite | improve this answer | |

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.