Imaginemos que en el curso de la implementación de una función se necesita intercambiar el valor de dos variables n y m de tipo int
ii) Completar de forma apropiada las lineas punteadas de la siguiente demostración de correctitud.

//estado E1
n = n - m;
//estado E2
//vale ...;
m = n + m;
//estado E3
//vale ...;
n = m - n;
//Estado E4
//vale ...;
//implica n == m@E1 ^ m == n@E1



¿Valdría la demostración si n y m fueran dos nombres para la misma variable(aliasing)?¿Por qué?

yo creo que no, porque en la 1º instrucción al modificar n queda n = 0, pero también modifica m porque m y n son referencias a una variable.
No se si esto es una demostración:

//estado E1
n = n - m;
//estado E2
//vale n = n@E1 - m
//dado q n y m reverencian al mismo valor m == n@E2 y n@E1 == m@E1
//implica n == m ==0

lo q contrastara con la implicación del estado E4 que espera q se diga n == m@E1 ^ m == n@E1

salvo que n y m referencien al valor 0