I1M2010: Trabajo en el entorno de prácticas

PorJosé A. Alonso

El objetivo de la clase es aprender a usar el entorno de trabajo del aula de informática. En concreto, aprender a

  • acceder a la cuenta personal en Ubuntu,
  • cambiar la contraseña,
  • descargar el enunciado de la relación de ejercicios,
  • abrir la relación de ejercicios en emacs y
  • resolver ejercicios.

En esta clase se han resuelto los 3 primeros ejercicios de la 2ª relación.

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

I1M2010: Definición de funciones

PorJosé A. Alonso

El objetivo de la clase de hoy es aprender a

  • definir funciones eh Haskell usando los patrones básicos de definición: composición, condicionales, guardas y patrones.
  • buscar funciones con Hoogle y ver su definición.
  • realizar el ciclo completo de definición de funciones en el cuaderno de ejercicios: descargar los enunciados, escribir la definición, comprobarla y publicarla en el cuaderno.

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

Las transparencias del tema son

Descargar (PDF, 203KB)

I1M2010: Introducción a la programación con Haskell

PorJosé A. Alonso

En la clase de hoy se ha visto el tema 2: Introducción a la programación con Haskell.

El objetivo del tema es aprender a:

  • usar Haskell como calculadora aritmética (con las funciones +, -, *, /, div y ^).
  • usar Haskell como calculadora de listas (con las funciones head, tail, take, drop, length, sum, product, ++ y reverse).
  • escribir guiones de Haskell en emacs.

Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 2º relación.

Las transparencias del tema son

Descargar (PDF, 204KB)

Aprender y enseñar

PorJosé A. Alonso

Hace poco me reencontré con una máxima de Tales de Mileto que figura desde hace tiempo en mi colección de citas. La máxima dice

De todo lo que es posible aprender, elige y aprende lo mejor; y de todo lo que hayas aprendido, elige lo mejor y enséñalo a los demás.

Esta máxima resume perfectamente los objetivos de Vestigium.

Formalizaciones en PVS y el problema de las versiones

PorJosé A. Alonso

En la wiki del Grupo de Lógica Computacional se han publicados las formalizaciones en PVS 4.2 de las siguientes teorías:

La adaptación la ha realizado María J. Hidalgo a partir de la versión de PVS 3.2. El proceso de adaptación ha sido complejo por las diferencias existentes entre ambas versiones de PVS. Los principales problemas que han aparecido son los siguientes:

  • Diferencia en el tratamiento de los juicios entre teorías situadas en distintos directorios y cargadas como extensiones del preludio.
  • Diferencia en las opciones por defecto en estrategias predefinidas.
  • Diferencia en el número de obligaciones de pruebas generadas.

Además, el problema de la compatibilidad entre las distintas versiones de los sistemas de razonamiento dificulta la reutilización de las teoría formalizadas. En concreto, en algunas teorías que hemos desarrollado se han usado teorías desarrolladas por otros como, por ejemplo, la teoría sobre puntos fijos de F. Bartels, A. Dold, F.W. v. Henke, H. Pfeifer y H. Rueß que está desarrollada en la versión 2.4 de PVS, no se ha adaptado a las siguientes versiones y no es adecuada para la versión actual de PVS.