Hola,
No me queda claro donde se definen y explican los predicados va_mapped_to_ma, is_RW, así como otros que se utilizan en las pre y post condiciones.
En una parte dice:
(the names of the auxiliary predicates used should be self-
explanatory).
Pero la verdad no me quedan del todo claros.
¿Alguien me podría dar una mano con esto?
Saludos,
Jairo.