Reseña: Certified HLints with Isabelle/HOLCF-Prelude

Se ha publicado un trabajo de verificación formal con Isabelle sobre Haskell titulado Certified HLints with Isabelle/HOLCF-Prelude.

Sus autores son Joachim Breitner, Brian Huffman, Neil Mitchell y Christian Sternagel.

El trabajo se presentará en el HART 2013 ( 1st International Workshop on Haskell And Rewriting Techniques).

Su resumen es

We present the HOLCF-Prelude, a formalization of a large part of Haskell’s standard prelude in Isabelle/HOLCF. Applying this formalization to the hints suggested by HLint allows us to certify them formally.

El códido del HOLCF-Prelude se encuentra aquí.

I1M2012: Ejercicios de razonamiento sobre programas

En las clases de ayer y hoy Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de la relación 31 en la que se plantean ejercicios de demostración por inducción de propiedades de programas. En concreto,

  • la suma de los n primeros impares es n^2,
  • 1 + 2^0 + 2^1 + 2^2 + … + 2^n = 2^(n+1),
  • todos los elementos de (copia n x) son iguales a x,
  • la equivalencia de las definiciones de factorial con y sin
  • acumulador,
  • amplia xs y = xs ++ [y].
  • numeroDeListasConSuma n = 2^(n-1),
  • fibItAux n (fib k) (fib (k+1)) = fib (k+n),
  • potencia x n == x^n,
  • reverse (xs ++ ys) == reverse ys ++ reverse xs,
  • reverse (reverse xs) = xs,

y por inducción sobre árboles binarios

  • espejo (espejo x) = x,
  • postorden (espejo x) = reverse (preorden x),
  • reverse (preorden (espejo x)) = postorden x,
  • nNodos (espejo x) == nNodos x,
  • length (preorden x) == nNodos x,
  • nNodos x <= 2^(profundidad x) - 1,
  • nHojas x = nNodos x + 1,
  • preordenItAux x ys = preorden x ++ ys

Estos ejercicios corresponden al tema 8 del curso.

Los ejercicios de la relación, junto con sus soluciones, se muestran a continuación
Read More “I1M2012: Ejercicios de razonamiento sobre programas”

I1M2012: Razonamiento sobre programas Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo demostrar propiedades de funciones definidas en Haskell. Los esquemas de demostración estudiados son:

  • por simplificación,
  • por casos,
  • por inducción sobre los números naturales,
  • por inducción sobre listas,
  • por inducción anidada y
  • por generalización e inducción.

Las transparencias usadas en la clase son las del tema 8:
Read More “I1M2012: Razonamiento sobre programas Haskell”

I1M20102 Ejercicios sobre la implementación en Haskell del TAD de los grafos mediante listas de pares

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando las soluciones a los ejercicios sobre la implementación en Haskell del tipo abstracto de datos de los grafos mediante listas de pares de la 29ª relación.

Los ejercicios y su solución se muestran a continuación
Read More “I1M20102 Ejercicios sobre la implementación en Haskell del TAD de los grafos mediante listas de pares”