Teórico/práctico: Damián Barsotti, Matías Lee.

Laboratorio: Martín Dominguez, Guillaume Hoffmann.

Teórico/Practico: lunes, aula 17, de 14 a 18 hs. Jueves, aula 25 de 14 a 16 hs. y aula 17 de 16 a 18 hs.

Laboratorio: miércoles de 9 a 13 hs., Lab. 30

• Creada aula virtual.

• Para regularizar la materia: 2 parciales aprobados o un recuperatorio equivalente con nota >= 4 y el taller aprobado.
• Para promocionar la materia: 2 parciales aprobados con nota >= 7, promedio >= 8 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 segundo cuatrimestre del año 2012.

• 25/4 y 17/6
• Recuperatorio 24/6.

• Notas primer parcial.
• Notas segundo parcial.
• Notas recuperatorio y condición final.
• Condición final de la materia.

• Examen Final 1.
• Examen Final 3.

• 11/3 Presentación de la materia. Derivación y verificación de programas. Practico 1. Expresiones Cuantificadas. Dado ejercicio 3 a. Pueden hacer hasta el ejercicio 4.

• 14/3 Reglas para la cuantificación general.

• 18/3 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).

• 21/3 Practico 2. Inducción. Demostración por inducción de propiedades. Inducción sobre listas. Hasta ej 2.

• 25/3 Derivación de recursión lineal. Hasta ejercicio 4.

• 28/3 Feriado

• 1/4 Feriado

• 4/4 Esquemas inductivos con ejercicio 5.

• 8/4 Ejercicio 6 de modularización. Suma de potencias en clase. Tuplas (ejercicio 7.a).

• 11/4 Generalizacion por abstraccion: ejercicio 8.a) psum.

• 15/4 Ejercicio sum_ant. Consulta. Hasta ej 9.

• 18/4 Segmentos. Ejercicio suma mínima de un segmento.

• 22/4 Consulta de práctico.

• 25/4 Parcial.

• 29/4 Practico 3 Modelo computacional imperativo. Hasta ej 2

• 2/5 Terna de Hoare. Weakesr Precondition. Wp de asignacion. Hasta ejercicio 3.e). Chun da wp del if

• 6/5 wp del if. Especificación y derivación. Hasta ejercicio 5.d

• 9/5 Teorema de la invariancia. Ej 5.e y f

• 13/5 Derivación de asignaciones y if (ej 6 y 7). Pueden hacer hasta el ejercicio 8.

• 16/5 Derivación mcd. Salte el ej 9 (arreglos)

• 20/5 Ej 9. Exp de ejercicio 10

• 23/5 Practico 4. Tecnicas para encontrar invariantes: termino de la conjunción. Ejercicios 1 y 2 en clase. Pueden hacer hasta el 4.

• 27/5 Técnica de reemplazo cte. por variable. Ej 6 y 6.a). Pueden hacer hasta ej 8

• 30/5 Técnica de predicados intermedios Ej 9 y 11.a)

• 3/6 Técnica de fortalecimiento de invariantes. Ej 12

• 6/6 Problemas de Borde.

• 10/6 Problemas de Borde.

• 13/6 Consulta/Repaso. Problemas de asignación de arreglos.

• 17/6 Parcial.

• 20/6 Feriado.

• 24/6 Recuperatorio.

• ¡Aprende Haskell por el bien de todos!
• Una introducción agradable a Haskell
• Hoogle, búsqueda de funciones por nombre o tipo.
• Using GHCI

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

• Why Functional Programming Matters John Hughes.
• Trampa en el cyberespacio.
• Software's Chronic Crisis.
• Voto electrónico. Los riesgos de una ilusión. Federico Heinz.
• X11 windows manager in Haskell!.

• Charla sobre Software Libre de Federico Heinz 6/5/2013.

• 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.

• 11/3 Presentación de la materia. Practico 1 (lógica). Expresiones Cuantificadas.
• 14/3 Reglas para la cuantificación general.
• 18/3 Pruebas de implicaciones y por casos.
• 21/3 Practico 2 (programación funcional). Inducción. Demostración por inducción de propiedades. Esquemas de inducción (k-induccion, induccion generalizada). Inducción sobre listas.
• 25/3 Derivación de recursión lineal
• 27/3 Corrección Proyecto 1 laboratorio.
• 28/3 Feriado
• 1/4 Feriado
• 4/4 Modularización. Esquemas inductivos.
• 8/4 Tuplas.
• 11/4 Generalizacion por abstraccion.
• 15/4 Consulta.
• 17/4 Corrección Proyecto 2 laboratorio.
• 18/4 Segmentos.
• 22/4 Repaso/Consulta.
• 25/4 Parcial.
• 29/4 Practico 3. Modelo computacional imperativo.
• 2/5 Ternas de Hoare.
• 6/5 Precondición más débil (weakest precondition).
• 9/5 Repetición (bucles). Teorema de la invariancia.
• 13/5 Derivación imperativa (asignación e if).
• 15/5 Corrección Proyecto 3 laboratorio.
• 16/5 Demostración con invariantes.
• 20/5 Repaso/Consulta.
• 23/5 Practico 4. Tecnicas para encontrar invariantes: termino de la conjunción.
• 27/5 Técnica de reemplazo cte. por variable.
• 30/5 Técnica de predicados intermedios.
• 3/6 Técnica de fortalecimiento de invariantes.
• 5/6 Corrección Proyecto 4 laboratorio.
• 6/6 Problemas de Borde.
• 10/6 Problemas de asignación de arreglos.
• 13/6 Consulta/Repaso
• 17/6 Parcial.
• 20/6 Feriado.
• 24/6 Recuperatorio.
• 26/6 Corrección Proyecto 5 laboratorio.

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 archivos del proyecto
• Proyecto 4
• Proyecto 5

• Introducción a la materia
• Proyecto 1:
  • Haskell, GHCI, secciones, map, filter, foldr
  • Tipos, error, clases de tipos
• Proyecto 2:
  • Proyecto 2: tipos de datos (archivo Haskell)
  • Activar los patrones n+k con ghci, ejemplo de chequeo que fact cumple con la propiedad dada en el práctico
• Proyecto 3:
  • Repaso sobre los tipos, Tipos Abstractos de Datos (TAD)
  • Ejemplo con case
  • Ejemplo de lista con invariante de orden
• Proyecto 4 / Proyecto 5:
  • Introducción a C
  • Código C: Hello, World!
  • Código C: Assignación múltiple
  • Código C: While
  • Código C: Mcd
  • Código C: Mcd con función
  • Código C: Arreglo, Inicialización
  • Código C: Struct, Struct 2
  • Introduccion a GDB. Por Marco Brunello y Leandro Ramos. Presentación, ejemplos.

Resumen de comandos de consola Linux y un libro sobre el tema.

• 11/3 Presentación de la materia. Derivación y verificación de programas. Practico 1. Expresiones Cuantificadas. Dado ejercicio 3 a. Pueden hacer hasta el ejercicio 4.
• 14/3 Reglas para la cuantificación general.
• 18/3 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).
• 21/3 Practico 2. Inducción. Demostración por inducción de propiedades. Esquemas de inducción (k-induccion, induccion generalizada). Inducción sobre listas. Hasta ej 2.
• 25/3 Derivación de recursión lineal. Hasta ejercicio 3.
• 28/3 Feriado
• 1/4 Feriado
• 4/4 Ejercicio 6 de modularización. Suma de potencias en clase. Esquemas inductivos con ejercicio 5.
• 8/4 Tuplas (ejercicio 7).
• 11/4 Generalizacion por abstraccion: ejercicio 8.a) psum.
• 15/4 Ejercicio sum_ant. Consulta.
• 18/4 Ejercicio suma mínima de un segmento. Consulta de práctico.
• 22/4 Consulta de práctico.
• 25/4 Parcial.
• 29/4 Practico 3 Modelo computacional imperativo. Hasta ej 2
• 2/5 Terna de Hoare. Weakest Precondition. Wp de skip, abort y asignacion. Hasta ejercicio 3.e)
• 6/5 wp del if. Especificación y derivación. Hasta ejercicio 5.d
• 9/5 Teorema de la invariancia. Ej 5.e y f
• 13/5 Derivación de asignaciones y if (ej 6 y 7). Pueden hacer hasta el ejercicio 8.
• 16/5 Derivación mcd. Salte el ej 9 (arreglos)
• 20/5 Ej 9. Exp de ejercicio 10
• 23/5 Practico 4. Tecnicas para encontrar invariantes: termino de la conjunción. Ejercicios 1 y 2 en clase. Pueden hacer hasta el 4.
• 27/5 Técnica de reemplazo cte. por variable. Ej 6 y 6.a). Pueden hacer hasta ej 8
• 30/5 Técnica de predicados intermedios Ej 9 y 11.a)
• 3/6 Técnica de fortalecimiento de invariantes. Ej 12
• 6/6 Problemas de Borde.
• 10/6 Problemas de Borde. Problemas de asignación de arreglos.
• 13/6 Consulta/Repaso
• 17/6 Parcial.
• 20/6 Feriado.
• 24/6 Recuperatorio.