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
//estado E1
n = n - m;
//estado E2
//vale n = n@E1 - m
//vale m = m@E1
//implica n = n@E1 - m@E1
m = n + m;
//estado E3
//vale m = n + m@E2
//vale n = n@E2
//implica m = n@E2 + m@E2
//implica m = n@E1 - m@E1 + m@E1
//implica m = n@E1
n = m - n;
//estado E4
//vale n = m - n@E3
//vale m = m@E3
//implica n = m@E3 - n@E3
//implica n = n@E1 - n@E2
//implica n = n@E1 - n@E1 + m@E1
//implica n = m@E1
//implica m = n@E1 ^ n = m@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