Hola, estoy trancado con este ejercicio. Seguí la recomendación de utilizar las reglas valid state v y vi pero no me sale. ¿Hay algún orden en particular en el que sea recomendable aplicarlas?
Saludos,
Jairo.
Hola.
La sugerencia es pensar la prueba conceptualmente primero, sin pensar en tácticas de Coq. Es una prueba simple. La clave es ver la información disponible (pre y post del Read) y las condiciones de validez de estado formalizadas.
Teniendo al menos una estructura conceptual de la prueba, la idea luego es ver cómo plasmarla en Coq (no es compleja ni larga, mas bien es conceptual).
Saludos, Carlos
Ya salió, si estaba pensándolo de esa forma. El pique (como me quedó a mi) era darse cuenta que dos direcciones de máquina eran la misma y por lo tanto las dos páginas de esas direcciones eran en realidad la misma.
Saludos,
Jairo.
Bueno, me alegro :)