Teórico/práctico: Damián Barsotti, Araceli Acosta, Franco Luque, Matías Lee, Mauricio Telechea, Demetrio Vilela.

Laboratorio: Gabriel Infante-Lopez, Martín Dominguez, Franco Luque, Cherini Renato, Leonardo Rodriguez.

Teórico: martes y jueves de 9 a 11 hs., Aula D1

Práctico: martes y jueves de 11 a 13 hs., Aula D1 D7

Laboratorio: viernes de 9 a 13 hs., Lab. 28

• Creada aula virtual.

• Para regularizar la materia: 2 parciales aprobados (o sus equivalentes recuperatorios) con nota >= 5 y el taller aprobado.
• Para promocionar la materia: 2 parciales aprobados (o sus equivalentes recuperatorios) con nota >= 7 y el taller aprobado.
• Para rendir libre la materia: seguiremos la modalidad del dictado ordinario de la materia, que aparece en “Condiciones para rendir libre el taller” en la página de la materia del año pasado.

Nota: El taller también se considerará aprobado si lo fue en el primer cuatrimestre del año 2012.

• 25/9 y 22/11
• Recuperatorio 29/11

• 21/8 Presentación de la materia. Derivación y verificación de programas. Expresiones Cuantificadas. Dado ejercicio 3 a. Pueden hacer hasta el ejercicio 4.
• 23/8 Reglas para la cuantificación general.
• 28/8 Ejercicio del rango unitario para N el cual introduce los conceptos de prueba de análisis por casos y pruebas de implicación descargando antecedentes. Esto último para B ⇒ E, B ⇒ E = E', B1 /\ B2 ⇒ E (usando intercambio).
• 30/8 Practico 2. Inducción. Hasta ej 2.
• 4/9 Derivación de recursión lineal. Hasta ejercicio 3.
• 6/9 Ejercicio 6 de modularización. Suma de potencias en clase. Esquemas inductivos con ejercicio 5.
• 11/9 Tuplas.
• 13/9 Generalizacion por abstraccion: ejercicio 8.a) psum.
• 18/9 Ejercicio sum_ant. Consulta.
• 20/9 Ejercicio suma mínima de un segmento. Consulta de práctico.
• 25/9 Consulta de práctico.
• 27/9 Parcial.
• 2/10 Estuve enfermo
• 4/10 Practico 3 Modelo computacional imperativo. Hasta ej 2
• 9/10 Terna de Hoare. Wp de skip, abort y asignacion. Hasta ejercicio 3.e)
• 11/10 wp del if. Especificación y derivación. Hasta ejercicio 5.d
• 16/10 Teorema de la invariancia. Ej 5.e y f
• 18/10 Derivación de asignaciones y if (ej 6 y 7). Pueden hacer hasta el ejercicio 8.
• 23/10 Derivación mcd. Salte el ej 9 (arreglos)
• 25/10 Ej 9. Exp de ejercicio 10
• 30/10 Practico 3. Tecnicas para encontrar invariantes: termino de la conjunción. Ejercicios 1 y 2 en clase. Pueden hacer hasta el 4.
• 1/11 Técnica de reemplazo cte. por variable. Ej 6 y 6.a). Pueden hacer hasta ej 8
• 6/11 Técnica de predicados intermedios Ej 9 y 11.a)
• 8/11 Técnica de fortalecimiento de invariantes. Ej 12
• 13/11 Problemas de Borde.
• 15/11 Problemas de Borde.
• 20/11 Problemas de asignación de arreglos.
• 22/11 Parcial

• Cosas básicas sobre Haskell
• Tutorial Haskell.
• Introducción a Haskell.
• Lenguaje de Programación Funcional Haskell.
• Wikipedia.

• Tutorial Haskell.
• Manual Hugs.
• Especificación del lenguaje Haskell 98.
• En la web.
• Hoogle. Búsqueda de funciones por nombre o tipo.

• En castellano pero básico.
• En ingles pero muy completo.
• Manual de referencia en inglés.
• Otro en castellano.

• Trampa en el cyberespacio.
• Software's Chronic Crisis.
• Implementing Functional Languages: a Tutorial. Simon L. Peyton Jones.
• Voto electrónico. Los riesgos de una ilusión. Federico Heinz.
• X11 windows manager in Haskell!.

• Digesto de axiomas y teoremas para cálculo proposicional y expresiones cuantificadas.

• Digesto para la programación imperativa.

• Práctico 1 - Repaso cálculo proposicional y expresiones cuantificadas.

• Práctico 2 - Especificación derivación y verificación de programas funcionales.

• Práctico 3 - Introducción a la programación imperativa.

• Práctico 4 - Programación imperativa.

• 21/8 Practico 1 (lógica). Expresiones cuantificadas (cuantificación generalizada).
• 23/8 Reglas generales para expresiones cuantificadas.
• 28/8 Pruebas por casos.
• 30/8 Practico 2 (programación funcional). Demostración por inducción de propiedades. Esquemas de inducción (k-induccion, induccion generalizada). Inducción sobre listas.
• 4/9 Derivación de programas con recursión lineal.
• 6/9 Reempazo constantes por variables y modularización.
• 7/9 Corrección Proyecto 1 lab.
• 11/9 Uso de tuplas. Inducción en dos parámetros.
• 13/9 Generalizacion por abstracción.
• 18/9 Segmentos.
• 20/9 Repaso.
• 25/9 Consulta y Parcial
• 27/9 Práctico 3. Modelo computacional imperativo.
• 28/9 Corrección Proyecto 2 lab
• 2/10 Ternas de hoare.
• 4/10 Precondición más débil (weakest precondition).
• 9/10 Repetición (bucles). Teorema invariancia.
• 11/10 Derivacion de asignaciones. Especificacion y derivacion de if.
• 16/10 Errores en programas imperativos. Demostración con invariantes.
• 18/10 Consulta de práctico
• 19/10 Corrección Proyecto 3 lab
• 23/10 Practico 4. Búsqueda de invariantes. Término de la conjunción.
• 25/10 Remplazo de constante por variable. Heurística para derivar un programas.
• 30/10 Consulta. Técnica de predicados intermedios: Ej 9 y 10.
• 1/11 Problemas de borde.
• 6/11 Recursión final.
• 8/11 Recursión final
• 9/11 Corrección Proyecto 4 lab
• 13/11 Repaso
• 15/11 Parcial imperativo
• 20/11 Update de arreglos. Repaso.
• 22/11 Recuperatorios
• 26/11 Corrección Proyecto 5 lab

El laboratorio consistirá en la aplicación práctica de los temas que se ven en la materia.

Aproximadamente clase de por medio, se tomará, en los últimos minutos de las clases, una pequeña evaluación (“parcialito”) que consistirá en uno o dos ejercicios similares (o iguales) a los que aparecen en los laboratorios. Estos ejercicios serán parte de la evaluación que determinará la aprobación del taller, necesario para la regularidad y promoción de la materia. Los parcialitos serán evaluados en “bien” (1), “regular” (0.5) o “mal” (0).

Para aprobar el taller, es condición necesaria tener el 70% de los puntos de los parcialitos. No todos los parcialitos tendrán la misma incidencia en la nota final, incidencia que se informará sobre el final del dictado de la materia.

* Proyecto 1.

* Proyecto 2.

* Proyecto 3 y los Archivos necesarios.

* Proyecto 4.

* Proyecto 5.

• Introducción a la materia
• Introducción a Haskell, parte 1
• Introducción a Haskell: sinónimos y tipos definidos
• Tipo Abstracto de Datos
• Introducción a C
• Configuración para Emacs.
• Conceptos necesarios para el proyecto 1
• Script que demuestra que el orden importa
• Conceptos necesarios para el proyecto 2
• Conceptos necesarios para el proyecto 3
• Conceptos necesarios para el proyecto 4

• 21/8 Practico 1 (lógica). Presentación de expresiones cuantificadas. Hasta cuantGen.
• 23/8 Reglas generales para expresiones cuantificadas. Pueden hacer todo el práctico 1.
• 28/8 Ejercicio del rango unitario para N el cual introduce los conceptos de prueba de análisis por casos y pruebas de implicación descargando antecedentes. Esto último para B ⇒ E, B ⇒ E = E', B1 /\ B2 ⇒ E (usando intercambio).
• 30/8 Practico 2 (programación funcional). Clase teórico/practica de 4 hs. Demostración por inducción de propiedades. Esquemas de inducción (k-induccion, induccion gen). Derivación de programas con inducción sin aplicar técnicas. Pueden hacer hasta ejercicio 5.
• 4/9 Derivación ejercicio sum del práctico. Técnica de análisis por casos en ejercicio de sumar los pares.
• 6/9 Modularización con ej del práctico: suma de potencias agregando parametro x. Está en el libro p173-176. No se da reemplazo de ctes por variables.
• 7/9 Corrección Proyecto 1 lab.
• 11/9 Tuplas con suma de potencias del libro. Generalización por abstracción con ej de cuadrado.
• 13/9 Ejemplo de generalizacion por abstraccion (p. 180). Practico listas iguales.
• 18/9 Ejemplo con segmentos. Dado sum_ant (ej b) con esta técnica (se supone que ya lo hicieron sin ella). Ejercicio 13 y 14 de práctica.
• 20/9 Practico
• 25/9 Practico
• 27/9 Práctico 3 (modelo computacional imperativo, sin busqueda de invariantes). Modelo computacional imperativo hasta ej 2. Consulta parcial en práctico.
• 28/9 Corrección Proyecto 2 lab
• 2/10 Ternas de hoare. Parcial
• 4/10 wp hasta if. Hasta ejercicio 5 d)
• 9/10 Bucle. Teorema invariancia. Hasta ej 5
• 11/10 Derivacion de asignaciones (ej 6). Especificacion y derivacion de if (ej 7)
• 16/10 Encontrar errores (ej 9). mcd (ej 11.a)
• 18/10 Ej 11.b.a
• 19/10 Corrección Proyecto 3 lab
• 23/10 Ej 11.b.b. Se podría haber comenzado el practico 4.
• 25/10 Practico 4. Término de la conjunción. Dado ej 1. Pueden hacer hasta el 4.
• 30/10 Remplazo de constante por variable. Dado ejercicio 5. Dado pasos heurísticos para derivar un programa. Pueden hacer hasta el 8.
• 1/11 Ej 5 y 6 como cuantificación generalizada. Ej 7 (minimo definido). Tecnica de predicados intermedios: Ej 9 y 10.
• 6/11 Ej de suma de los anteriores igual al elemento y de máxima diferencia de elementos.
• 8/11 Repaso
• 9/11 Corrección Proyecto 4 lab
• 13/11 Parcial Imperativo
• 15/11 Update de arreglos: ej 20. Repaso.
• 20/11 Recuperatorios
• 26/11 Corrección Proyecto 5 lab