Trabajo Práctico sobre Verificación de Software
Enunciado del TP.
Atelier-B, herramienta para escribir especificaciones B.
El intérprete Prolog SWI-Prolog.
El intérprete {log}. El zip incluye el manual de usuario de {log}.
Presentación/Tutorial (en inglés) sobre {log}
El apunte de clase que explica cómo traducir de B a {log}, cómo hacer simulaciones, demostraciones y generación de casos de prueba con {log}.
El apunte de clase que explica cómo traducir de Z a {log}, cómo hacer simulaciones, demostraciones y generación de casos de prueba con {log}.
(Solo para alumnos que hayan regularizado IS 1 antes de 2026 y que rindan IS 2 hasta el 1/3/2027)
Una biblioteca para trabajar en {log} con listas representadas como conjuntos. Este archivo conviene ponerlo en el mismo directorio donde pongan {log}.
Especificación B de la agenda de cumpleaños y la traducción a {log}.
Especificación Z de la agenda de cumpleaños y la traducción a {log}.
Página oficial de {log}.
Dos ejemplos de TPs resueltos en 2019 que pueden tomar como referencia: Antonio Locascio y Mercedes Castro. Tener en cuenta que actualmente el enunciado del TP y {log} son diferentes a los de 2019.