Next revision | Previous revisionNext revisionBoth sides next revision |
teaching:cc5115 [2020/02/10 12:08] – created folmedo | teaching:cc5115 [2020/02/10 12:56] – [Motivación y Objetivos] folmedo |
---|
====== Análisis y Verificación de Programas (CC7126) ====== | ====== Programación funcional (CC5115) ====== |
| |
| |
==== Motivación y Objetivos ==== | ==== Motivación y Objetivos ==== |
| |
Los problemas en las piezas de software pueden acarrear consecuencias catastróficas, tanto a nivel económico como de la seguridad de las personas. La validación y verificación de software juegan, por lo tanto, un rol fundamental en el proceso de desarrollo. En particular, para el proceso de verificación se ha recurrido históricamente a diversas técnicas de //testing//. Si bien el testing representa un enfoque muy eficiente para detectar bugs, su alcance está limitado a probar la //presencia// de bugs, y no su //ausencia//. | El propósito de este curso es introducir la //programación funcional//º a través del lenguaje Haskell. La programación funcional es reconocida por dar lugar a un estilo mucho más declarativo –y elegante– de programación, y tres características que la hacen particularmente atractiva son su conveniencia para //verificar// programas, razonando algebraicamente de la misma manera que lo hacemos en matemática, para //paralelizar// la ejecución de programas, ganando órdenes de magnitud en eficiencia, y por último, para //abstraer// patrones de programación recurrentes, generando código más compacto, robusto y reusable. |
| |
| Lenguajes populares como Java, JavaScript o Scala han sabido explotar estas características adoptando un enfoque multi-paradigma. Para los objetivos de este utilizaremos sin embargo Haskell, un lenguaje puramente funcional. Haskell se considera en la frontera del diseño de lenguajes de programación y hoy en día tiene una penetración no menor en la industria, siendo usado por compañías como Microsoft, Facebook, IBM, Galois, AT&T, JaneStreet y la NASA. |
| |
En este curso estudiaremos el análisis y verificación formal de programas, que constituyen un conjunto de herramientas matemáticas para razonar //formalmente// sobre el comportamiento de los programas. A diferencia del testing, su empleo permite //demostrar//--en el sentido matemático--que los programas son correctos y se adhieren a su especificación. | A lo largo del curso cubriremos tanto la práctica como la teoría de la programación funcional. Al finalizar el mismo, los estudiantes serán capaces de: |
| * escribir programas funcionales usando el lenguaje Haskell; |
| * explotar un sistema de tipos estático, de características avanzadas; |
| * hacer un uso sofisticado de la recursión, para resolver problemas no-triviales; |
| * reconocer, encapsular y explotar diversos patrones de programación recurrentes; |
| * escribir programas que se ejecutan de manera paralela; |
| * reconocer y explotar diversas oportunidades de optimización, y |
| * testear programas de manera automática, usando la librería QuickCheck. |
| |
A lo largo del curso presentaremos los fundamentos matemáticos subyacentes a dichas herramientas, reconociendo, en particular, sus alcances y limitaciones. Estudiaremos, además, las distintas estrategias que se utilizan para automatizar su aplicación. | Para un listado más detallado de los temas abordados en el curso consultar {{teaching:cc5115:programa_cc5115.pdf|programa del curso (CC5115)}}. Para una discusión más a fondo sobre la relevancia y beneficios de la programación funcional consultar el artículo {{teaching:whyofy.pdf|Why functional programming matters}}. |
| |
| |
==== Contenido ==== | |
Al término del curso, el estudiante manejará las nociones de: | |
* **Semántica formal de programas:** reconocerá dos estrategias clásicas para describir rigurosamente el significado o efecto de un programa. | |
* **Verificación formal de programas:** será capaz de demostrar (en el sentido matemático) la corrección funcional de un programa mediante el uso de lógica de Hoare y razonar también sobre programas que manipulan estructuras de datos dinámicas mediante el uso de lógica de separación. | |
* **Análisis estático de programas:** será capaz de razonar formalmente sobre propiedades más generales de los programas, de manera completamente automática, y en tiempo de compilación. | |
| |
| |
==== Elegibilidad ==== | ==== Elegibilidad ==== |
Curso electivo para Doctorado en Computación, Magíster en Ciencias de la Computación e Ingeniería Civil en Computación. | Curso electivo para Ingeniería Civil en Computación. |
| |
| |
==== Requisitos ==== | ==== Requisitos ==== |
CC4101 Lenguajes de Programación / Autorización (contactar [[folmedo@dcc.uchile.cl|Federico]]).\\ El curso no presenta ningún requisito adicional, aunque será de gran ayuda cierto grado de madurez matemática por parte del alumno. | Algoritmos y estructura de datos (CC3001) y matemáticas discretas para la computación (CC3101). |
| |
| |