RA2013: Razonamiento automático sobre programas con Isabelle/HOL
En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar automáticamente propiedades de programas funcionales con Isabelle/HOL.
En primer lugar, se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las transparencias del tema 7 del curso de Programación declarativa (de 3º del Grado en Informática). Como lectura complementaria se recomienda el capítulo 13 del libro de G. Hutton Programming in Haskell.
A continuación se ha explicado cómo demostrar automáticamente las propiedades anteriores con Isabelle/HOL.
El enunciado de las propiedades es inmediato: basta escribir la palabra lemma y a continuación la propiedad entre comillas dobles; por ejemplo,
|
1 |
lemma "longitud (repite n x) = n" |
También se puede poner un nombre al lema, por ejemplo,
|
1 2 |
lemma inversaAcAux_es_inversa: "inversaAcAux xs ys = (inversa xs)@ys" |
La demostración es la palabra by seguida por el método de demostración. Los métodos que hemos usado son
- by simp: que es el método de simplificación por reescritura,
- by (induct x) auto: que es por inducción en x (donde x es un número natural o una lista) y simplificación automática de ambos casos,
- by (induct rule: fn.induct) auto: que es por inducción según la definición de la función fn y simplificación automática de todos los casos,
- by (cases x) auto: que hace distinción de casos según el tipo x y simplificación automática de todos los casos,
- by (induct x arbitrary: y) auto: que es por inducción en x (donde y se considera una variable arbitraria) y simplificación automática de todos los casos y
- by (simp add: lema_auxiliar): que es el método de simplificación por reescritura añadiéndole a las reglas de reescritura la correspondiente al lema_auxiliar,
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2013: Razonamiento automático sobre programas con Isabelle/HOL”
,