I1M2010: Ejercicios de recursión en Haskell (2)

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos seguido aplicando las heurísticas estudiadas en el tema 6 para resolver ejercicios ejercicios de la 8ª relación.

Los ejercicios resueltos han sido 7.1 (mezcla), 7.2 (ordenada), 7.3 (prop_mezcla_ordenada), 8.1 (borra), 8.2 (prop_borra), 9.1 (esPermutacion), 9.2 (prop_InversaEsPermutacion), 9.3 (prop_mezcla_permutacion), 10.1 (mitades), 10.2 (ordMezcla), 10.3 (prop_ordMezcla_ordenada) y 10.4 (prop_ordMezcla_pemutacion).

Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los restantes ejercicios de la 8ª relación y los ejercicios de la 9ª relación.

El tipo abstracto de datos de las pilas en Haskell

PorJosé A. Alonso

En este artículo continúo la serie dedicada a los tipos de datos abstractos (TAD) en Haskell presentando el TAD de las pilas.

En artículos anteriores presenté los TAD de los polinomios y el de los conjuntos. En éste voy a presentar el TAD de las pilas y sus implementaciones en Haskell.

Al igual que hice en los anteriores TAD, usaré módulos, funciones de escritura y QuickCheck para conseguir la abstracción, independencia y certificación de los resultados de las implementaciones.

El contenido del resto del artículo es el siguiente: el TAD de las pilas, las implementaciones en Haskell mediante tipos algebraicos y mediante listas y la comprobación con QuickCheck de sus propiedades.
Read More “El tipo abstracto de datos de las pilas en Haskell”

Trabajo de Lógica Computacional en Grenoble

PorJosé A. Alonso

El grupo VDS (Verification & Modeling of Digital Systems Group) del Laboratorio TIMA (Techniques de l’Informatique et de la Microélectronique pour l’Architecture des systèmes intégrés) en Grenoble ha anunciado la ogerta de una plaza de trabajo: Formal methods for verifying dependability properties for a secured architecture.

El trabajo se desarrollará dentro del proyecto SHIVA (Secured Hardware Immune Versatile Architecture) y será dirigido por Laurence Pierre.

Los objetivos del trabajo serán la especificación de la propiedades de seguridad necesarias para los módulos hardware desarrollados por otros equipos del proyecto, la mejora de la especificación y de las metodologías de la verificación y su aplicación a las tareas verificadas.

Un precedente del trabajo es la verificación formal de comunicaciones en redes de chips con ACL2.