3.2 Resolving references to variables to constants

If there are any ``chainable'' equalities, you should try to get everything resolved to constants whenever possible. For example, let us consider the following post condition:

$\rm {post(1)} = (x < y) \wedge (y = 10)$

Here, we already know, for sure, that $y$ has a value of 10. This means that the inequality $(x < y)$ can now be resolved as $(x < 10)$. The main purpose to do this is to decouple variables from each other. In other words, we want to lessen the impact of a change to one variable to conditions that involve other variables.

In this example, a later assignment can change the value of $y$. However, that will not impact the fact that we already know that $(x < 10)$.