bcardiff
-
2008-05-29
Menu
▾
▴
#4 Avance incorrecto cuando hay aliasing
la traducción de
call S[e, e]
donde
program S[a, b : univ]
{
UpdateVar[b, a]; // 1
UpdateVar[b, a]; // 2
UpdateVar[b, a]; // 3
UpdateVar[a, b] // 4
}
genera:
S[e_0,e_1,e_1,e_2,e_3]
fijando relaciones incorrectas entre los distintos estados.
Esta situación es regular que aparezca en la traducción de Java a DynJAlloy en sentencias como:
x = method(x);