ISIS 4215 Métodos Formales en Algorítmica
Métodos formales (matemáticas aplicadas) en la especificación, el diseño y el desarrollo de programas. El tema de tipos abstractos de datos ecuacionales (TADs) se presenta como soporte teórico de la programación orientada a objetos. Tales TADs se pueden considerar como especificaciones formales en un sistema de reescritura de términos, y su implementación es útil en el desarrollo de prototipos rápidos. Estos prototipos pueden desarrollarse de manera natural en lenguajes funcionales o de reescritura de términos (Lisp, CAML, …), pero también pueden usarse en lenguajes imperativos con recursión. Para mejorar su desempeño, los prototipos pueden transformarse manteniendo su semántica y, por ende, su corrección. Los lenguajes de programación imperativos y aún los orientados a objetos se basan en el modelo procedimental de solución de problemas. En general, se pretende resolver un problema mostrando el cambio de estado de las variables del programa. Los programadores deben especificar cómo se resuelve un problema. En contraposición los lenguajes declarativos se preocupan más en la descripción del problema. De cierta forma, la especificación del problema es ya la solución. Dos de estos paradigmas son el paradigma lógico y el paradigma funcional. Los tipos de abstractos de datos ecuacionales se pueden implementar directamente en los lenguajes funcionales haciendo más rápido el desarrollo de prototipos. Los lenguajes lógicos se pueden usar para implementación sencilla de sistemas inteligentes.
Página del catálogo en este curso