En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede escribir en Isabelle/Isar demostraciones de la lógica proposicional.
En la clase se ha presentado desde la página 15 a la 21 de los apuntes
Read More “RA2010: Razonamiento proposicional con Isabelle”
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”
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.
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos aplicado las heurísticas estudiadas en el tema 6 para resolver ejercicios los 6 primeros ejercicios de la 8ª relación.
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.
En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos visto patrones recursión:
Además, hemos visto una heurística para definir funciones por recursión.
Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 8ª relación.
Las transparencias usadas en la clase son las comprendidas entre las páginas 13 y 30 del tema 6
Read More “I1M2010: Patrones de definiciones por recursión en Haskell”