FUN: una herramienta did´ actica para la derivaci´ on de programas funcionales Araceli Acosta1 , Renato Cherini1 , Alejandro Gadea1 , Emmanuel Gunther1 , Leticia Losano1,2 , and Miguel Pagano1,2 1

FaMAF - Univ. Nacional de C´ ordoba 2 CONICET {aacosta,cherini,gadea,gunther,losano,pagano}@famaf.unc.edu.ar

1.

Introducci´ on

Existen diversas razones que nos llevan a reflexionar sobre las problem´aticas del aprendizaje de la programaci´on en contextos universitarios y de la formaci´on universitaria de los profesionales de la programaci´ on. Por un lado, en el presente contexto donde el sector TIC tiene una incidencia cada vez mayor sobre el PBI nos debemos preguntar sobre las capacidades de la industria del software para brindar soluciones de calidad y proveer garant´ıas de la correcci´on de los productos; en particular teniendo en cuenta la creciente importancia de m´etodos formales en la industria [11]. En este sentido es importante reflexionar sobre c´omo la curr´ıcula de las carreras de computaci´on ayuda a desarrollar las habilidades necesarias que permitan a sus estudiantes y egresados comprender las bases te´ oricas y utilizar las herramientas pr´ acticas que permiten producir software confiable. Por otro lado, la obligatoriedad de la educaci´ on secundaria – establecida en la ley 26.206 – favorece que ingresen a la universidad estudiantes con distintos recorridos escolares, en particular en lo que respecta a las habilidades l´ ogicomatem´aticas. Esto nos presenta el desaf´ıo de lograr una mayor permanencia de los estudiantes en las carreras manteniendo el nivel de excelencia y calidad. Para este prop´osito puede ser de gran utilidad la incorporaci´on de tecnolog´ıas de la informaci´ on a la ense˜ nanza [9]. En este trabajo se describe la utilizaci´on de una herramienta desarrollada para la ense˜ nanza de l´ogica y programaci´on, que esperamos poner a prueba en el aula durante el pr´ oximo a˜ no. En la secci´on 2 se presentan el contexto de utilizaci´on de la herramienta y se aborda la perspectiva did´actica; en la secci´on 3 se describen los conceptos b´asicos a ense˜ nar con esta herramienta. En la secci´on 4 se describe la utilizaci´ on de la herramienta con ejemplos. En la secci´ on 5 cerramos con las conclusiones de nuestro trabajo.

2.

Una perspectiva para ense˜ nar programaci´ on

El primer curso de programaci´ on en la carrera de la Lic. en Cs. de la Computaci´on de Fa.M.A.F es “Introducci´on a los algoritmos” y se dicta en el primer

2

Araceli Acosta et al.

semestre de primer a˜ no. El objetivo de este curso es introducir la programaci´ on en peque˜ na escala como la transformaci´ on de especificaciones formales en programas ejecutables; las habilidades que se espera los estudiantes adquieran son la capacidad de modelar problemas formalmente, el uso de la l´ogica como herramienta para razonar sobre y probar la correcci´on de programas. El dictado de este curso tiene una interesante experiencia acumulada durante diez a˜ nos y fruto de ello es el libro [3], utilizado como material principal durante el semestre. Esta experiencia tambi´en se traduce en ciertas miradas reflexivas sobre el curso. Desde 2007 se han desarrollado investigaciones focalizadas en este curso [8, 4] que permitieron comprender mejor los procesos de aprendizaje involucrados en el mismo y delinear algunas de las dificultades experimentadas por los estudiantes. A partir de entrevistas a estudiantes, en [4] se rescatan algunas percepciones de los estudiantes: (i) una importante discontinuidad entre los contenidos y las formas de estudio propias de la escuela secundaria y las de la universidad, en particular este curso; (ii) dificultades, particularmente en los primeros meses, para mantener el ritmo de estudio; (iii) frecuentes impedimentos para avanzar en la resoluci´on de los ejercicios debidas a la falta de conocimiento de los detalles del lenguaje de programaci´ on. En [8] se analiz´o c´omo los alumnos iban construyendo demostraciones formales, qu´e estrategias empleaban y qu´e recursos utilizaban; develando que “la construcci´ on de una prueba no sigue el car´ acter lineal que posee una prueba una vez finalizada”. Para los estudiantes elaborar una demostraci´ on era un proceso con idas y vueltas donde se recurr´ıa a compa˜ neros y profesores y se utilizaban artefactos, principalmente el listado de axiomas del c´alculo. El proceso implicaba realizar c´alculos auxiliares, probar distintos caminos –algunos infructuosos– y la discusi´ on con los colegas del curso. Teniendo en cuenta estas dificultades, se inici´o el proyecto Theona [1] con el objetivo de desarrollar material pedag´ ogico y herramientas did´acticas inform´aticas que faciliten los procesos de aprendizaje de los alumnos en el curso. En estos dos a˜ nos se desarroll´o, financiados parcialmente por Fonsoft, el material de texto y cuatro herramientas did´ acticas: Equ permite realizar demostraciones, autom´aticamente verificadas, de f´ormulas ecuacionales. Sat ayuda a comprender el significado de f´ ormulas l´ogicas de primer orden que involucren cuantificadores a trav´es la adecuaci´on de mundos de objetos geom´etricos y propiedades de dichos modelos expresados en f´ormulas l´ogicas. Fun permite derivar programas funcionales a partir de especificaciones formales; y tambi´en verificar la correcci´on de programas. Hal es un asistente de construcci´on de programas imperativos con el uso de sistemas asercionales. 2.1.

Introducci´ on a la programaci´ on funcional

La curricula a abordar con la herramienta consta de dos unidades tem´aticas: introducci´on a elementos de l´ogica y especificaciones y derivaci´on de programas

FUN: una herramienta did´ actica para la derivaci´ on de programas funcionales

3

funcionales. El motivo de esta elecci´on es que el proceso de desarrollo de software en la peque˜ na escala puede basarse en la especificaci´on del problema en una f´ ormula l´ ogica (complicada, por cierto) y que a partir de esa f´ormula se pueden realizar manipulaciones simb´ olicas para obtener otra expresi´on formal: el programa que resuelve en forma algor´ıtmica el problema especificado en la f´ormula. Otra perspectiva que admite este curso es la verificaci´on de programas: dados una especificaci´on y un programa (digamos programado por otro estudiante), c´omo podemos convencernos que el mismo satisface su especificaci´on. Para ello, podemos utilizar la misma maquinaria l´ ogica para demostrar que el programa efectivamente computa lo que la especificaci´on prescribe. L´ ogica para especificaciones La primera unidad tem´atica est´a dedicada a los elementos de la l´ogica necesarios para poder escribir especificaciones. El ´enfasis est´a puesto en los elementos que componen un lenguaje formal, primero a trav´es de la introducci´on de un lenguaje de expresiones aritm´eticas, para pasar luego a un lenguaje de f´ ormulas y el sistema de pruebas de esta l´ogica. Notemos que en este contexto el estudiante se enfrenta por primera vez a ciertos elementos que son comunes a cualquier lenguaje de programaci´on: constantes, operadores y su aridad, variables, un elemental sistema de tipos y una gram´atica que definen las frases v´ alidas del lenguaje. Pensamos que esta primera aproximaci´on a los fen´omenos sint´acticos en una l´ogica proposicional tiene la ventaja de no lidiar directamente con un lenguaje de programaci´ on. La elecci´on del lenguaje de expresiones aritm´eticas tiene como ventaja que uno puede explicar informalmente la sem´antica de las expresiones (y de las f´ormulas) sin necesidad de introducir nociones de modelos; la noci´ on de pruebas es, b´asicamente, una secuencia de ecuaciones justificadas por proposiciones (ya sean axiomas, teoremas o hip´ otesis), donde cada paso ecuacional es correcto si los t´erminos de la ecuaci´on coinciden sint´acticamente con la justificaci´on. Tambi´en en este momento se discuten las nociones de satisfacci´on y validez, nuevamente pensando en la sem´ antica natural de las expresiones aritm´eticas. En una segunda etapa se extiende la l´ogica proposicional a l´ogica de predicados tipada; ´esta incluye cuantificadores l´ogicos y aritm´eticos, tales como la sumatoria, la productoria y el conteo. En este pasaje aparecen nuevos conceptos sint´acticos que tambi´en son comunes a lenguajes de programaci´ on, en particular la noci´on de ocurrencias libres y ligadas de variables, renombre de variables ligadas, sustituci´on. Con las expresiones cuantificadas se introducen las especificaciones de funciones que, a trav´es de razonamientos ecuacionales, ser´an transformados en expresiones del lenguaje de programaci´on funcional. Programaci´ on funcional El lenguaje de programaci´ on, descrito en la sec. 3.1, permite la declaraci´ on de funciones a trav´es de constantes, operadores, patternmatching y recursi´ on mutua. La noci´on de computaci´on en este tipo de lenguajes se basa en la reducci´on de expresiones hasta llegar a los valores, o formas can´ onicas. Este paradigma de programaci´on tiene la ventaja de ser cercano a la pr´actica matem´atica que se tiene habitualmente, en tanto el orden de las reducciones no afecta el valor final de la computaci´on, puesto que no hay una manipulaci´on de

4

Araceli Acosta et al.

un estado; en este sentido las “variables” del lenguaje son variables matem´aticas en tanto su valor no var´ıa durante la ejecuci´on del programa.

3.

Conceptos b´ asicos

En esta secci´ on daremos un descripci´ on general de los conceptos a abordar mediante la utilizaci´on de la herramienta. Estos conceptos se fundamentan en lo descripto en la secci´ on anterior.

3.1.

Lenguaje de programaci´ on

El lenguaje de programaci´ on que utilizaremos es un lenguaje funcional con una sintaxis similar a Haskell. Este lenguaje incluye expresiones aritm´eticas y expresiones booleanas proposicionales. Por ejemplo, se puede definir la funci´on de elevar al cuadrado de la siguiente manera cuadrado : Int → Int cuadrado.x = x ∗ x Uno de los aspectos m´as distintivos de la programaci´on funcional son las definiciones recursivas de funciones sobre tipos inductivos (Hudak [7] ofrece una interesante introducci´on a este y otros aspectos de lenguajes funcionales). Los tipos inductivos que incluye el lenguaje son los naturales y las listas. El lenguaje permite definiciones utilizando patrones (pattern matching). Por ejemplo, puesto que las listas de elementos de tipo a son un tipo inductivo (con constructores [], para el caso base, y x . xs, para el caso inductivo con x : a y xs : [a]), podemos definir la funci´on sum para sumar todos los elementos de una lista de enteros de la siguiente manera sum : [Int] → Int sum.[] = 0 sum.x . xs = x + sumar.xs Existen una serie de operadores predefinidos para las expresiones aritm´eticas, booleanas y para operar sobre listas. Ejemplos de operadores sobre listas son concatenar dos listas (+ + ), calcular la cantidad de elementos de una lista (#), etc. Notemos que a cada definici´ on que hemos dado la acompa˜ nan expresiones que determinan el tipo de la funci´on. El chequeo est´atico de tipos ayuda tanto a detectar errores tempranamente como a la legibilidad de la funci´on. Por otro lado, desde el punto de vista did´actico, el tipado de expresiones y funciones es una herramienta importante con la que cuentan los estudiantes para la elaboraci´ on de nuevas funciones.

FUN: una herramienta did´ actica para la derivaci´ on de programas funcionales

3.2.

5

Sistema formal

El objetivo de un sistema formal es explicitar un lenguaje en el cual se realizar´an demostraciones y las reglas para construirlas. Esto permite tener una noci´on muy precisa de lo que es una demostraci´on, as´ı tambi´en como la posibilidad de hablar con precisi´on de la sintaxis y la sem´antica de las expresiones y f´ormulas del lenguaje. En una materia introductoria a la programaci´ on estos conceptos son importantes, dado que un lenguaje de programaci´on es un sistema formal. El dise˜ no de este sistema formal permite, por un lado, demostrar la correcci´on de programas y derivar programas a partir de su especificaci´on, ya que el lenguaje de programaci´on est´ a incluido en el mismo; y por otro lado, nos permiti´o desarrollar una herramienta autom´ atica de verificaci´on de demostraciones y derivaciones de los programas. Adem´as de las expresiones aritm´eticas, booleanas proposicionales y sobre listas, incluidas en el lenguaje de programaci´on, se agregan las expresiones cuantificadas; que son de mucha utilidad para la especificaci´ L on de programas y propiedades. Una expresi´on cuantificada tiene la forma h x : R.x : T.xi que se entiende como T.x0 ⊕ T.x1 ⊕ T.x2 ⊕ . . . donde xi satisface el predicado R. Los cuantificadores utilizados P Q son el “para todo” (∀), el “existe” (∃), la sumatoria ( ), la productoria ( ) y el contador (N ). Para especificar, por ejemplo, la funci´on sum que se defini´o recursivamente en la secci´ on anterior, se puede utilizar la siguiente expresi´on cuantificada: X sum.xs = h i : 0 6 i < #.xs : xs.ii 3.3.

Reglas de inferencia y demostraciones

Para completar el sistema formal se definen una serie de axiomas y teoremas b´asicos, demostrados a partir de los axiomas, y un sistema deductivo basado en la l´ogica ecuacional al estilo de Dijkstra [5], que utiliza la transitividad y la regla de Leibniz como reglas de inferencia, y se introduce el m´etodo inductivo cuando est´ an implicados tipos inductivos. Los axiomas sobre los que se trabaja son un conjunto de f´ ormulas para la l´ogica proposicional y para la l´ogica de cuantificadores. Para la aritm´etica se axiomatizan algunas propiedades sobre los n´ umeros naturales, necesarias para demostraciones inductivas, mientras que otras propiedades se dejan a criterio del estudiante, es decir, se pueden utilizar como paso en una demostraci´ on, pero no se verifican formalmente. Una demostraci´ on dentro del sistema formal consiste en probar la validez de una f´ormula mediante una serie de pasos justificados con axiomas y teoremas ya demostrados. A continuaci´ on se muestra un ejemplo particular de la aritm´etica: (x > 0) ∨ (x 6 0) ≡ { Aritm´etica } (x > 0) ∨ ¬(x > 0) ≡ { Tercero excluido (P ∨ ¬P ≡ T rue) } True

6

3.4.

Araceli Acosta et al.

El proceso de construcci´ on de programas

En la actualidad es ampliamente aceptado que el proceso de construcci´on de programas debe dividirse en al menos dos etapas: la etapa de especificaci´ on del problema y la etapa de desarrollo del programa o de programaci´ on. Este enfoque tiene sus ra´ıces en las nociones de programaci´ on transformacional [10] y c´ alculo de refinamientos [2]. El resultado de la primera etapa es una especificaci´ on formal del problema, la cual sigue siendo abstracta (poco detallada) pero est´ a escrita formalmente. La segunda etapa da como resultado un programa y una demostraci´on de que el programa es correcto respecto de la especificaci´ on dada. A esta demostraci´on se la llama verificaci´ on. Por ejemplo, a continuaci´on se muestra la demostraci´on de la correcci´ on de la funci´on sum cuya especificaci´on y definici´on recursiva se introdujo anteriormente. La demostraci´on consiste en una prueba que, para cualquier lista xs, la funci´on sum satisface la especificaci´on, es decir computa efectivamente la suma de los elementos de la lista. Esta demostraci´ on se puede hacer a partir de los axiomas y teoremas b´asicos del formalismo y utilizando el principio de inducci´on. El caso basePsupone P que la lista es vac´ıa. En esta situaci´on la especificaci´on se convierte en .[ ] = h i : 0 6 i < #[ ] : [ ]!ii que es trivialmente verdadero, pues ambos t´erminos son iguales a 0 por definici´on. Para el caso inductivo la especificaci´ on toma la forma: X sum.(x . xs) = h i : 0 6 i < #(x . xs) : (x . xs)!ii que se demuestra a continuaci´on P h i : 0 6 i < #(x . xs) : (x . xs)!ii = { Definici´ P on de # } h i : 0 6 i < 1 + #xs) : (x . xs)!ii = { Teorema separaci´ P on del primer t´ermino } (x . xs)!0 + h i : 0 6 i < #xs : (x . xs)!(i + 1)i = { Definici´ Pon de ! } x + h i : 0 6 i < #xs : xs!ii = { Hip´ otesis inductiva } x + sum.xs = { Definici´ on de sum } sum.(x . xs) 3.5.

Derivaci´ on de programas

Hasta aqu´ı se desarrollaron tres etapas para la construcci´on de un programa. En primer lugar, elaborar una especificaci´on formal para el mismo. En segundo lugar, construir el programa. En tercer lugar, dar una demostraci´on de que dicho programa satisface la especificaci´on. A la construcci´on en simult´aneo del programa y de su verificaci´on se la llama derivaci´ on. En este proceso se parte de una especificaci´on formal de una funci´on

FUN: una herramienta did´ actica para la derivaci´ on de programas funcionales

7

y a trav´es de transformaciones de la expresi´on se encuentra la definici´on de una funci´on computable que satisface la especificaci´on gracias a buenas propiedades del sistema ecuacional. Esta metodolog´ıa fue desarrollada a partir de los trabajos de E.W.Dijkstra. En la secci´on 4 se describe un ejemplo de derivaci´on en el entorno de programaci´ on FUN.

4.

FUN: una herramienta did´ actica

FUN es una herramienta que consiste en un IDE (entorno de desarrollo integrado) para escribir programas y pruebas en un lenguaje que permite definir progamas funcionales, especificaciones de programas, realizar pruebas matem´aticas utilizando l´ogica proposicional y de predicados, y realizar derivaciones de programas de acuerdo con los conceptos introducidos en la secci´ on anterior. A continuaci´ on describimos FUN a trav´es de algunas capturas de pantallas.

Figura 1: La pantalla principal de FUN

En la secci´on central de la pantalla est´ a el editor de programas y pruebas, a su derecha se dispone de la lista de axiomas a utilizar como justificaci´on en las pruebas; mientras que el panel izquierdo lista los m´odulos cargados y sus componentes. Debajo del editor se encuentran las consolas de informaci´on y de evaluaci´on; en el inferior de la ventana se presentan botones para poder ingresar caracteres de los s´ımbolos matem´ aticos m´as usados en las especificaciones y las pruebas.

8

Araceli Acosta et al.

Como dijimos, el programa permite escribir y chequear pruebas del c´alculo proposicional y de predicados. Las pruebas se realizan mediante la declaraci´ on de teoremas. Por ejemplo consideremos el teorema de doble negaci´on ¬¬p ≡ p, ver la Fig. 2b. Para realizar la prueba de ¬¬p ≡ p se utiliza un teorema auxiliar

(a) Teorema auxiliar

(b) Doble negaci´ on

Figura 2: Demostraciones de teoremas

teo1, Fig. 2a. Para justificar los pasos de la prueba, el usuario puede utilizar una cantidad de axiomas seleccion´andolos mediante la interfaz o escribiendo literalmente sus nombres, puede utilizar teoremas ya probados previamente o hip´ otesis, y tambi´en puede utilizar definiciones de funciones. Una vez que se escribe un m´odulo (un archivo que contiene definiciones de funciones, demostraciones y/o especificaciones) el usuario puede chequear que el mismo sea correcto y la herramienta mostrar´a la lista de todas las declaraciones indicando con una tilde si la misma es correcta, Fig. 3a o con un s´ımbolo negativo cuando no lo es, Fig. 3b. Si alguna declaraci´on tiene un error, cuando se hace click sobre la misma en el panel izquierdo, se muestra en la consola de informaci´on la raz´ on por la cual la misma no es correcta, Fig. 3c. La derivaci´on de funciones en el entorno FUN sigue el mismo proceso que se explic´ o en la secci´ on anterior; en las Figs. 4a y 4b se muestran respectivamente los casos bases e inductivos de la derivaci´ on de la sumatoria de una lista. Como se puede ver, en ambos casos la expresi´ on final no contiene cuantificadores y por lo tanto es un programa evaluable. El lenguaje funcional subyacente a FUN fue definido y estudiado formalmente en [6]; utilizando la sem´antica operacional all´ı definida se implement´ o el evaluador integrado en el entorno. El usuario puede evaluar una expresi´on paso-a-paso hasta la expresi´ on can´ onica.

REFERENCIAS

(a)

9

(b)

(c)

Figura 3: M´odulos y sus definiciones

5.

Conclusiones y trabajos futuros

En el art´ıculo hemos presentado una metodolog´ıa para la ense˜ nanza de programaci´on enfatizando la importancia de contar con una especificaci´on formal. El aporte m´ as novedoso de este art´ıculo es la herramienta FUN, que permite al estudiante realizar la derivaci´on, programaci´on y verificaci´on en un u ´nico entorno. La herramienta le brinda al estudiante la posibilidad de corregir sus propias derivaciones sin necesidad de la supervisi´on de un docente. En el pr´oximo a˜ no se espera utilizar el material de estudio producido y las herramientas inform´aticas en el dictado del curso “Introducci´on a los algoritmos”. A partir del uso intensivo de las herramientas se contar´a con un importante feedback para mejorarlas, tanto en funcionalidades como en interfaz. En otras l´ıneas de trabajo se est´ an desarrollando herramientas que complementan estos contenidos curriculares. En particular, se est´a desarrollando una herramienta, HAL, que persigue los mismos objetivos que FUN pero orientada a la programaci´on imperativa; esto implica un cambio completo de paradigma. Esta herramienta permitir´a completar con los contenidos conceptuales de un curso introductorio de programaci´on desde la perspectiva formal.

Referencias [1] Araceli Acosta y col. Proyecto Theona. http://www.theona.com.ar/. Mayo de 2013.

10

REFERENCIAS

(a)

(b)

Figura 4: Derivaci´on de sum

[2] Ralph-Johan Back y Joakim Wright. Refinement Calculus. New York, NY: Springer New York, 1998. [3] Javier Blanco, Silvina Smith y Dami´an Barsotti. C´ alculo de Programas. Universidad Nacional de C´ordoba, 2009. [4] Javier Blanco y col. “An introductory course on programming based on formal specification and program calculation”. En: SIGCSE Bull. 41.2 (jun. de 2009), p´ ags. 31-37. [5] David Gries. “Equational logic as a tool”. En: Algebraic Methodology and Software Technology. Ed. por V. S. Alagar y Maurice Nivat. Vol. 936. Lecture Notes in Computer Science. Springer Berlin Heidelberg, 1995, p´ ags. 1-17. [6] Emmanuel Gunther. “Entorno para la Derivacion de Programas”. Tesis de lic. Universidad Nacional de C´ordoba - Facultad de Matem´atica, Astronom´ıa y F´ısica, jul. de 2013. [7] Paul Hudak. “Conception, evolution, and application of functional programming languages”. En: ACM Comput. Surv. 21.3 (sep. de 1989), p´ags. 359-411. [8] Leticia Losano. “Procesos situados de aprendizaje en cursos b´ asicos deprogramaci´on: volverse miembro de una comunidad”. Tesis doct. Universidad Nacional de C´ordoba - Facultad de Filosof´ıa y Humanidades, abr. de 2012. [9] Mariana Maggio. Enriquecer la ense˜ nanza: Los ambientes con alta disposici´ on tecnol´ ogica como oportunidad. Buenos Aires: Paidos, 2012. [10] Helmut A. Partsch. Specification and Transformation of Programs. Berlin, Heidelberg: Springer Berlin Heidelberg, 1990. [11] Mari¨elle Stoelinga y Ralf Pinger, eds. Formal Methods for Industrial Critical Systems. Vol. 7437. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012.