 This illustrates that the result of the sequence \(z := x\); \(x := y\); \(y := z\) is that the values of \(x\) and \(y\) are swapped, with the side effect that the old value of \(z\) gets lost. In other words, the meaning of the program \(z := x\); \(x := y\); \(y := z\) can be viewed as a mapping from an input machine state \(s\) to an output machine state \(s'\) that differs from \(s\) in several respects: \(s'(x) = s(y)\) and \(s'(y) = s(x)\) (that is, the input values of \(x\) and \(y\) are swapped in the output state), and \(s'(z) = s'(y)\).