Open project position at TUM: Computer-supported verification of automata constructions

PorJosé A. Alonso

El grupo Foundations of Software Reliability and Theoretical Computer Science de la Universidad Politécnica de Munich ha anunciado la oferta de una plaza de trabajo en Lógica Computacional: Open project position at TUM: Computer-supported verification of automata constructions

El objetivo del trabajo es la realización de una biblioteca formalmente verificada con Isabelle de algoritmos de verificación de modelos (en inglés, model checking). El proyecto se enfoca en la aproximación a la verificación de modelos basada en automata. Por tanto, para su realización se será necesario formalizar en Isabelle los conceptos habituales de la teoría de automata.

Los directores del proyecto son Javier Esparza, Tobias Nipkow y Jan-Georg Smaus.

I1M2010: Segundo examen de la evaluación continua

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha realizado el segundo examen de la evaluación continua.

Las notas se han publicado en la WebCT.

En la página de la asignatura se han publicado las soluciones del examen.

El resumen estadístico del resultado del examen es el siguiente

No presentados 12
Suspensos 5 25%
Aprobados 3 15%
Notables 6 30%
Sobresalientes 6 30%
Total 32

El porcentaje de aprobados (sobre presentados) es 75.0 y la nota media es 7.1.

Desarrollo del comando wc de Unix en Haskell

PorJosé A. Alonso

wc (en referencia a los términos ingleses “word count”) es un comando utilizado en el sistema operativo Unix que se utiliza para saber el número de palabras, líneas y caracteres de un fichero. Por ejemplo, si tenemos un fichero ciudades.txt cuyo contenido es

podemos contar con wc sus líneas, palabras y caracteres como sigue

En Haskell se pueden desarrollar programas simples con análogo comportamiento. Por ejemplo se puede contar las líneas del fichero como sigue

El contenido del programa CuentaLineas.hs es simplemente

Read More “Desarrollo del comando wc de Unix en Haskell”

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

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 y de la 9ª relación

De la 8ª relación se han resuelto los ejercicios 11.1 (sum’), 11.2 (prop_sum), 12.1 (take’), 12.2 (prop_take), 13.1 (last’), 13.2 (prop.last), 14.1 (mcd), 14.2 (prop_mcd_equiv), 14.3 (prop_mcd), 14.4 (prop_mcd_div), 15.1 (menorDivisible), 15.2 (divisiblePorTodos), 15.3 (prop_menorDivisible) y 15.4 (euler5).

De la 9ª relación se han resuelto los ejercicios 1.1 (sumaCuadrados), 1.2 (prop_SumaCuadrados), 1.3 (sumaCuadrados’), 1.4 (prop_sumaCuadrados), 2.1 (numeroBloques), 2.2 (numeroBloques’), 3.1 (sumaCuadradosImparesR), 3.2 (sumaCuadradosImparesC) y 4.2 (cifras).

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

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.