DAO2012

En la sesión de hoy del seminario Demostración asistida por ordenador (DAO2012) se ha presentado cómo se puede demostrar con Isabelle propiedades de programas.

En el tema 8 del curso de I1M vimos cómo se puede razonar sobre programas funcionales. Hoy hemos visto cómo Isabelle puede hacer automáticamente las demostraciones de dicho tema. Los métodos que hemos usado son

• simplificación (con simp),
• automático (con auto),
• inducción sobre números naturales y listas (con induct),
• inducción con variables libres (con arbitrary) y
• inducción en varias variables (con induct rule).

La teoría correspondiente a la clase es T3_Razonamiento_sobre_programas.thy cuyo contenido se muestra a continuación
Read More “DAO2012: Razonamiento sobre programas con Isabelle”

En la sesión de hoy del seminario Demostración asistida por ordenador (DAO2011) se ha presentado Isabelle como un sistema de programación funcional que permite

• evaluar expresiones aritméticas y lógicas (con value),
• definir funciones no recursivas (con definition),
• definir funciones recursivas (con fun),
• enunciar propiedades (con lemma) y
• demostrar propiedades por simplificación (con simp).

La teoría correspondiente a la clase es T2_Programacion_funcional_en_Isabelle.thy cuyo contenido se muestra a continuación
Read More “DAO2012: Programación funcional en Isabelle”