Programación imperativa vs declarativa III (Demostración Automática de Teoremas)

¿Cuantas veces nos hemos encontrado (los programadores) con un bug “raro”, esa conjunción astral que hace que nuestro software, tras meses e incluso años sin mostrar síntomas de debilidad, cruja cual madera reseca por el paso del tiempo?. ¿Cómo demostrar al cliente que no fallará más?, ¿y si hay vidas de personas dependientes de la no existencia de errores en un software como en el caso de Karen Sandler?.

¿Te habías fijado que en cuestión de software no es posible asegurar la ausencia de bugs?. Una vez escrito un código, todas las estrategias tradicionales se basan en la repetición de los procesos de verificación (eg. el código que ha escrito un programador es revisado por otros tantos) o en test que sólo pueden validar una parte muy pequeña del dominio funcional del proceso (eg. una función para sumar dos enteros de 32 bits posee un dominio de 2⁶⁴ elementos, revisarlos todos le llevaría a un procesador a 3GHz 195 años ¡y es una suma!).

¿Será la Demostración Automática de Teoremas la solución a todos los males?.

Demostrar la calidad del software

Excepto en matemáticas, no existen las verdades absolutas (eg. en física, la probabilidad de que ahora mismo te aparezca delante de las narices una manzana ¡no es estrictamente cero!). En matemáticas sin embargo, dadas unas premisas (axiomas), es posible demostrar sin ningún tipo de duda, ciertos resultados (no cualquier resultado y únicamente en base a esos axiomas). Afortunadamente para nosotros, la programación forma parte de las matemáticas y, en principio, nada impide (y de hecho se hace) demostrar que un algoritmo sea correcto, sin tacha, libre de bugs.

Claro que no es lo mismo demostrar que un algoritmo concreto está libre de bugs, a demostrar que todo nuestro sistema (en el que se han escrito muchas líneas y por muchas personas diferentes) está libre de bugs. No porque no se pueda hacer, sino porque conlleva un tiempo y esfuerzo tan enorme, que nadie puede permitírselo (hablo de aplicaciones con una cierta envergadura).

Si alguien demuestra que su código (algoritmo) está libre de bugs, no tiene que realizar ningún test, ninguna prueba para validarlo, de igual forma, que no hace falta contar todos los números naturales para demostrar (sin ningún genero de duda) que hay infinitos números naturales.

¿El código se puede “demostrar”?

Tradicionalmente, cuando se habla de demostrar algo, se habla de que alguien (eg. un matemático), aclare tanto como sea necesario una determinada afirmación (teorema), de forma que “siguiendo el hilo” de su explicación, no quede lugar a dudas de la exactitud de cada uno de los pasos. Otro matemático, puede tomar la demostración del anterior y seguir cada uno de los pasos para ver si es correcta o no.

En realidad, cuando nosotros escribimos un programa, ¡estamos demostrando algo!. Efectivamente, nuestro código, es la prueba fehaciente y por escrito, de que dada una entrada, se producirá una salida determinada. Cuando estamos revisando el código de un compañero, realmente estamos siguiendo estos pasos para ver si está “bien demostrado” y que, efectivamente, dada una entrada, se producirá la salida esperada.

Comparemos la conversación para resolver un problema (usando demostraciones, claro) entre matemáticos y entre programadores:

Matemáticos	Programadores
Alguien dice “me gustaría saber cuanto vale la suma de los números entre 1 y N (incluidos)”.
Pepe: “si tomas el primer y último elementos suman N+2, si tomas el segundo y penúltimo suman N+2 y así sucesivamente, como hemos tomado los sumandos dos a dos, tenemos N/2 veces N+2, luego la suma total es N(N+2)/2”	Juan: “si tomas las variables S=1, I=1 y mientras sea I<=N haces S=S+I, obtienes la suma buscada”
Luis: “te equivocas, la suma entre el primer y último elementos es N+1, pues el primer elemento es 1 y el último es N; la suma entre el segundo y el penúltimo es N+1 pues el segundo es 2 y el penúltimo N-1 y así sucesivamente, la suma total es por tanto N(N+1)/2”	Pedro: “te equivocas, antes de empezar a sumar ninguno de los números, la suma acumulada vale cero, pues aún ninguno de los números ha sido tomado en cuenta, debes empezar con S=0”
Pepe: “¡es verdad!”	Juan: “¡tienes razón!”

Así, podemos fijar dos ideas básicas:

• Nuestro código, es una demostración (¡o intento de, claro!), son los pasos a un nivel del que no hay genero de duda de su validez (cada instrucción soportada por el lenguaje ¡y todos pensamos que nuestro lenguaje no tiene bugs!).

• Cuando hablamos de “demostrar que mi código está libre de bugs”, realmente lo que estamos demostrando es que nuestro código, nuestra demostración del problema original es correcta. Es decir, siendo estrictos, la demostración ya está hecha (nuestro código); lo que pasa es que suele ser tan compleja la verificación, que al problema de verificarlo también se le llama “queda demostrado que el código está libre de bugs”. Por ejemplo, Luis y Pedro han demostrado que Pepe y Juan tenían errores en sus demostraciones (en sus códigos).

Demostración Automática de Teoremas

La Demostración Automática de Teoremas es una rama difícil, incipiente y compleja que, no obstante, da cada vez mejores frutos. En su versión más “sencilla” y fructífera, se trataría no de encontrar una demostración, sino de revisarla (acuérdate de las dos ideas que hemos fijado anteriormente). El código, junto con los requisitos que debe cumplir, formarían el “teorema” y el sistema validaría automáticamente dicho teorema indicando si, efectivamente, el código aportado implica los requisitos (burdamente explicado, sea dicho de paso).

Un ejemplo notable es seL4, una familia de micro-núcleos (en los que se basan los sistemas operativos Unix, incluido Android). El “resumen” del trabajo realizado lo puedes encontrar aquí, pero yo destacaría a modo de resumen (del resumen):

• “it is suitable for real-life use, and able to achieve performance that is comparable with the best-performing microkernels”. (seL4 es válido para uso real y su rendimiento es similar a aquellos con los mejores rendimientos).

• “its behaviour is precisely formally specified at an abstract level”. (Su funcionamiento está especificado formalmente a nivel abstracto).

• “its formal design is used to prove desirable properties, including termination and execution safety”. (Su diseño formal es usado para demostrar propiedades deseables, incluyendo la terminación y ejecución confiables).

• “its implementation is formally proven to satisfy the specification”. (Se comprueba formalmente que su implementación satisface la especificación).

• “its access control mechanism is formally proven to provide strong security guarantees”. (Se comprueba formalmente que los mecanismos de control de acceso son muy seguras).

Aunque seL4 no sea una demostración formal “al uso” (eg. ver figura 1 del ciclo de diseño) y pudieran ponerse pegas a la calidad del producto debido a la arbitrariedad de las propiedades deseables (no hay un criterio formal para seleccionar las propiedades deseables), no cabe duda que la formalización es un hito importante, porque quedan demostradas, fuera de toda duda, esas mismas propiedades (sean ideales o no). Es decir, no es preciso revisar repetidamente el código ni lanzar innumerable número de pruebas unitarias para asegurar sin lugar a dudas que el código cumple con las especificaciones.

Desde el punto de vista de la calidad del software (asegurar que seL4 cumple los requisitos), no hay mejor solución.

(Nota 1: por supuesto podría haber un error en el proceso que invalide el trabajo realizado, de la misma forma que Pepe y Juan tenían errores en sus demostraciones, pero eso sólo invalidaría el caso práctico, no la aplicación teórica).

(Nota 2: digo que pueden ponerse pegas al producto, porque seL4 es un kernel de un sistema operativo y sus estructura, elegida para resolver el problema de la gestión de los recursos de una máquina, no han sido seleccionados mediante un procedimiento formal; Dios puede venir perfectamente y entregar otra muchísimo mejor ¡pero Dios no podrá detectar fallos en la calidad de seL4 en base a los requisitos establecidos!).

seL4 no es el único caso práctico en que se ha modelado formalmente un sistema para realizar demostraciones automatizadas (o validaciones de la “demostración / formalización”). Tras el famoso error Pentium FDIV, parece ser que los fabricantes de procesadores incluyen demostración automática de algunas propiedades de sus procesadores (eg. Intel). Programas como Isabelle han sido usados por Hewlett-Packard para verificar el diseño del bus de sus servidores HP 9000, encontrando errores que habían pasado todas las pruebas y simulaciones previas. En el lenguaje Lightweight Java, se ha verificado formalmente que no se producen errores de tipo (ver referencias) y seguro que hay otros muchos ejemplos y muy interesantes que yo desconozco.

El problema de la Demostración/Verificación Automática de Teoremas

En general (y hasta donde yo se), no existen métodos generales y eficientes para verificar teoremas, es decir, no se conoce aún el algoritmo de Dios para verificar teoremas (ya no digamos para demostrarlos). En el caso más sencillo de verificar teoremas dentro de la lógica proposicional, el problema es co-NP-completo y por tanto la solución general pasa por asumir un coste exponencial. Eso quiere decir, que las soluciones actuales pasan por aprovechar el conocimiento concreto que se tenga del problema concreto a resolver (y no uno general), es decir, serán soluciones muy complejas (como en cálculo simbólico, normalmente). Aquí, puedes ver a los medallistas en este terreno.

Aun así, podemos ver un par de ejemplos (burdos y simplones si) para hacernos una idea, de como pueden ser las estrategias que se siguen y darnos cuenta, que son más precarias (menos elegantes, generales, útiles, …) que cuando hablábamos de cálculo simbólico.

Si conoces Prolog te resultarán familiares los ejercicios típicos en los que se establecen ciertas relaciones como las típicas hijo(X, Y) :- padre(Y, X). y abuelo(X, Z) :- padre(X, Y), padre(Y, Z). y tras indicar una serie de datos (como padre(pedro, juan).), se le pueden hacer preguntas para que el sistema las evalúe automáticamente, por ejemplo “¿es luis el abuelo de juan?” mediante algo como ?-abuelo(luis, juan)..

Prolog directamente, sólo trabajará sobre el conjunto de datos aportado (no demostrará nada general), pero las preguntas que se le hagan, serán ciertas dentro de ese conjunto de datos. Por ejemplo, si nosotros estamos seguros de tener una población cargada en Prolog (padres, hijos, tíos, …) representativa (no tiene porqué ser grande) de todas las relaciones familiares de interés, podremos estar seguros, sin lugar a dudas, que sabrá demostrar cosas como “el hijo de un abuelo que tiene un nieto ¿es padre de ese nieto?” (obviamente no, puede ser tío), sin que nosotros tengamos que revisar todas las posibilidades. (Como lo haga Prolog es otra cosa). Las demostraciones por exhaución son perfectamente válidas y muchas demostraciones contienen pasos por exhaución.

Microsistema de verificación de teoremas

A modo de ejemplo y simplificando la estrategia de Prolog, vamos a crear un “microsistema” que nos permita demostrar (dejar en claro, sin lugar a dudas un resultado sin tener que especificar nosotros los casos de prueba) dos resultados muy sencillos.

Nuestro microsistema va a ser una versión reducida de lo que hace Prolog (en 50 líneas de javascript no se hacer nada mejor), dudaba de si poner el código inline (porque no es trivial y puede entenderse sin él) pero a los programadores siempre nos gusta verlo, por tanto aquí está; este es nuestro microsistema de validación automática:

En primer lugar definimos nuestro lenguaje formal (las primeras 29 líneas), que no es más, que lógica proposicional:

• A siempre_que B, sinónimos serían sii, igual_que o ==.

• no A, es la negación o NOT booleano.

• A y B, conjunción o el AND booleano.

• A o B, disyunción o el OR booleano.

• A implica_que B, implicación, SI A, entonces fijo que SI B.

• ( A ), anidamiento de expresiones.

Con dicho lenguaje formal, nuestro sistema solicita dos conjuntos de proposiciones: las proposiciones que forman nuestro programa, nuestro código (el que queremos validar), al que llamamos REGLAS y por otro lado, las proposiciones que queremos verificar en base a dichas reglas, a las que llamaremos CONSULTAS.

En realidad, las CONSULTAS nos sirven tanto para validar (si yo se que cierta proposición debe ser cierta, entonces si nuestro sistema nos dice que no es cierta, habremos deducido que hay un error en nuestro programa) como para obtener información de nuestro programa (podemos consultar una proposición y simplemente ver la respuesta que nos da el sistema).

El procedimiento de verificación es sencillo (las 16 líneas siguientes): para combinación (cierto/falso) de todas las variables involucradas que cumplan las reglas, se verifican las consultas, si alguna combinación falla en alguna consulta, esa consulta es falsa (que puede ser lo que se espera, no obstante).

Verifiquemos dos programas (forzosamente triviales) para ver como funciona, para ello, puedes ver localmente la página completa de nuestro microsistema validador desde aquí.

Paraguas y días lluviosos

Hablar de lógica proposicional y no mencionar los paraguas y los días lluviosos es de mala educación, por eso vamos a verificar (con nuestro microsistema) que hemos codificado bien las reglas que nos indican cuando debemos llevar o no paraguas.

En base a unos requisitos muy complejos que no caben en este post, hemos codificado las siguientes reglas para saber cuando debemos llevar o no paraguas (ésto son las reglas):

• esta_nuboso siempre_que (no llueve y no hace_sol)

• llevo_paraguas siempre_que (no esta_nuboso)

Como la lista de requisitos es muy amplia, sólo pondremos dos de ellos, que vienen a decir que, el hecho de que llevemos paraguas, no nos dice nada acerca de si el día está soleado o de si está lluvioso, es decir, nuestro validador deberá decir que son falsas las siguientes dos condiciones, de lo contrario, nuestro código (las reglas) estarán mal codificadas:

• llevo_paraguas implica_que hace_sol (debe ser falsa)

• llevo_paraguas implica_que llueve (debe ser falsa)

Cuestión de vida o muerte

El otro ejemplo que quiero poner, en realidad es hasta mas sencillo, pero cuya formulación, si no lo has visto antes, hace que parezca mucho más difícil. Se trata del siguiente problema:

“Te encuentras encerrado en una habitación que posee dos puertas indistinguibles, una de ellas te permite escapar con seguridad, mientras que la otra te lleva a una muerte inminente. En cada puerta hay un soldado que no impedirá que accedas a la puerta, es más, se te permite hacer una única pregunta a sólo uno de los soldados. El problema está en que uno de los soldados es un mentiroso compulsivo y el otro el exponente máximo de la sinceridad pero claro, ellos también son indistinguibles a simple vista. ¿Cómo saldrías vivo de la habitación?”

Puedes estrujarte un rato el cerebro (en cuyo caso deja de leer inmediatamente porque voy a dar la solución) y puede que caigas o puede que no en la solución, que no es más que preguntar a uno de los soldados: qué te diría el otro, si le preguntaras si la puerta de la salvación es una concreta, y entonces, hacer lo contrario de la respuesta que obtengas. En realidad, sólo se trata de una doble negación.

Si lo se, la solución (el algoritmo que tenemos que codificar) es casi ininteligible, por eso es ideal para que, una vez codificado, nuestro microsistema nos diga si está correctamente codificado o no ¡nos asegurará que siempre obtendremos la respuesta correcta!. Veamos entonces nuestro programa (las reglas) que resuelve el misterio y nos permite salvar la vida:

• pregunto_mentiroso siempre_que (no salgo_vivo)

• pregunto_sincero siempre_que salgo_vivo

• pregunto_mentiroso_diria_sincero siempre_que (no pregunto_sincero)

• pregunto_sincero_diria_mentiroso siempre_que pregunto_mentiroso

• elijo_contrario_mentiroso_sincero siempre_que (no pregunto_mentiroso_diria_sincero)

• elijo_contrario_sincero_mentiroso siempre_que (no pregunto_sincero_diria_mentiroso)

Las reglas son una traslación del procedimiento, pero como no sabemos si la pregunta se la haremos al sincero o al mentiroso, en nuestro programa codificamos los dos casos. Quizás la única aclaración es la variable “salgo_vivo”, que no está fijada en ningún sitio, realmente no hace falta, porque representa la puerta por la que preguntamos, aunque lo normal será preguntar por la puerta que nos dará la libertad.

Así, tome la decisión que tome (“elijo_contrario_mentiroso_sincero” o “elijo_contrario_sincero_mentiroso”), deberá de darme como respuesta la puerta por la que he preguntado, es decir, deben cumplirse (ser ciertas) las dos siguientes consultas a nuestro sistema:

• elijo_contrario_mentiroso_sincero implica_que salgo_vivo

• elijo_contrario_sincero_mentiroso implica_que salgo_vivo

Eso es, haga la pregunta a quien la haga (al mentiroso o al sincero) siempre salgo vivo ¡¿no es genial?!.

Programación imperativa vs declarativa

(En el siguiente post de la serie, meditaremos en mayor profundidad sobre qué es ser imperativo y qué es ser declarativo. Confío que captarás el enfoque de las siguientes reflexiones en su sentido general, sin intentar aplicarlo a ningún caso concreto, fuente inagotable de ambigüedades y malentendidos).

Como hemos visto, se están produciendo importantes avances en la validación automática de sistemas cada vez más complejos. La esperanza, obviamente, es poder validar de forma totalmente automática un lenguaje de propósito general que pueda ser usado en la industria.

Nada impide que algún genio establezca unos criterios de formalización de las estructuras tradicionalmente imperativas (for, while, if, …) que permitan de forma eficiente, validar todos los programas actualmente existentes, pero no es probable.

El lenguaje imperativo, es una traslación directa de las herramientas físicas de las que se dispone actualmente (los procesadores) y su diseño por tanto está acomodado a los procesos físicos y no a los procesos de diseño de software, por tanto los primeros, imponen restricciones a los segundos (la máquina de Turing o el juego de la vida no tienen de forma explícita las estructuras mencionadas [for, while, if, …] sin embargo, desde el punto de vista de diseño de software son equivalentes en cuanto a la capacidad de poder producir un resultado, un programa).

En el otro lado, están los lenguajes formales (que por definición son declarativos… en su ámbito) cuyo diseño proviene de una meditada y sesuda conjunción de relaciones y teoremas, sin (a priori) limitaciones debidas a elementos externos y por tanto, cada uno de sus resultados está demostrado (hay problemas abiertos, obviamente) formando una estructura coherente sobre la que se espera alcanzar el Nirvana del desarrollo de software.

En GenBeta Dev | Programación imperativa vs declarativa I, Programación imperativa vs declarativa II (Cálculo simbólico)
Más información | Demostración matemática, Automated theorem proving, Propositional logic, Prolog, Co-NP-completo
Más información | seL4, Isabelle, Intel, Lightweight Java