Camilo Chacón Sartori - Computación y programación funcional

Esta definición podría parecer obvia, al menos en su primera parte. Sabemos que un algoritmo no es una entidad humana o biológica, pero que sí puede afectar la vida de estas (principalmente con sistemas de inteligencia artificial). A continuación, dice que los algoritmos «son entidades abstractas»; esto nos da a entender que existe, para él, una relación directa con las matemáticas, que son el lenguaje de las entidades abstractas. Pero ¿qué tipo de entidad abstracta?

Nosotros definiremos el algoritmo desde un punto de vista formal siguiendo la afirmación de Gurevich, en conjunto con lo que menciona Leslie Lamport 6 en su publicación «Who Builds a House Without Drawing Blueprints?» («¿Quién construye una casa sin dibujar los planos?»):

Necesitamos entender la tarea de programar a un nivel más alto antes de empezar a escribir código. (Lamport, 2015)

Concordamos con Lamport, por eso seguiremos su línea de pensamiento en este capítulo para tratar con los algoritmos, en busca de ese «nivel más alto».

Existen dos formas de ver lo que es un algoritmo: (1) desde un punto de vista de la especificación, es decir, la fase previa a implementarlo en un lenguaje de programación y donde podemos expresar nuestras soluciones usando el lenguaje universal de la ciencia: las matemáticas, o (2) la implementación de un algoritmo en un lenguaje de programación tradicional. Las dos no son excluyentes.

La capacidad de resolver problemas computacionales no implica que se deba usar el punto (2) sin el (1). Este es un error clásico de personas que están totalmente orientadas a la tecnología. En cambio, si seguimos la forma de trabajar de grandes informáticos del siglo XX, nos daremos cuenta de que usar las matemáticas para expresar nuestras ideas es enriquecedor y que, posteriormente, nos acercaremos a la parte de la implementación con mayor convicción y la posibilidad de cometer menos errores, ya que la rigurosidad es prioritaria y enriquecedora.

Ahora bien, la especificación hace referencia a algo formal, concreto, no simplemente a una lista de requerimientos junto a sus «posibles» soluciones. No; la idea es definir matemáticamente cómo funcionará el algoritmo para, así, evitar los posibles errores en una futura implementación. La implementación es involucrarnos directamente en los detalles de la herramienta para hacer realidad dicha especificación. Lamentablemente, en algunos círculos de programadores se tiende a omitir la primera etapa, tanto por responsabilidad personal (interna) como desde la empresa donde se trabaja (externa). Reducir el tiempo de desarrollo se prioriza a toda costa, aun dejando de lado la calidad que viene ligada a la especificación. Esto trae consigo una debilidad en el desarrollo de software, porque no se piensa antes de programar. Por ello, a continuación, analizaremos la fase de especificación.

La especificación es la búsqueda de la exactitud ( correctness en inglés) de un sistema computacional. Indudablemente, no es algo nuevo a la hora de construir algoritmos. Existen diversas formas de aplicarla, una de ellas, y la más clásica, es la verificación formal.

Puesto que hoy en día existe una omisión casi completa de este tema, es lo que explicaremos a continuación. Creemos que será de gran ayuda para un programador o programadora a quien le interese conocer nuevas técnicas para validar sus algoritmos y no tan solo usar pruebas unitarias como un mecanismo unívoco de aproximación a la reducción total de errores.

Dentro de la computación tenemos la ingeniería de software, que es un área particularmente relacionada con el ciclo de vida de un producto, la gestión de personas, la metodología de desarrollo, la planificación y el diseño de pruebas, entre otras labores. Y dentro de la misma tenemos la verificación de software, la cual es una disciplina dividida en dos categorías: estática y dinámica.

La verificación formal es parte de la estática, y la dinámica está relacionada al conocido proceso de testing para encontrar errores ( bugs en inglés) en un software (aunque esta última se podría ver más como una «validación» que una verificación).

La verificación formal es un área que trata sobre la correctitud de un algoritmo; es decir, hace referencia a si un algoritmo cumple o no con su especificación. Un algoritmo es correcto si cumple lo siguiente: (1) hace lo que dice la especificación; (2) los valores de entrada generan los valores «correctos» de salida, y (3) se ejecuta en un tiempo finito (es decir, evita caer en el problema de la parada [se refiere a que no se puede determinar si un algoritmo entrará en un ciclo infinito que nunca terminaría de ejecutarse]).

Esta área fue introducida por Robert W. Floyd en su artículo «Assigning Meanings to Programs» («Asignar significados a los programas»). Por medio de aserciones lógicas se comprueba la validez de un algoritmo haciendo uso de pruebas de correctitud, equivalencia y terminación. El mismo autor menciona en dicho artículo: «este documento intenta proporcionar una base adecuada para las definiciones formales de los significados de los programas en los lenguajes de programación apropiadamente definidos.».

Cada instrucción de un algoritmo es comprobada a través de expresiones lógicas (aserciones). Es decir, podemos comprobar la validez de un algoritmo en el ámbito de la especificación sin necesidad de ejecutarlo para saber si devolverá el valor correcto. Es por esto que se trata de una verificación estática.

Por su mismo mecanismo, la verificación formal es más compleja de realizar que el testing , ya que se debe pensar y analizar exhaustivamente cómo trabajará cada algoritmo, a través de un conjunto de aserciones bien definidas, desde los argumentos de entrada hasta los de salida. Una técnica formal que nos ayuda a trabajar con esto es la llamada lógica de Hoare.

Lógica de Hoare

Tony Hoare, en su artículo «An Axiomatic Basis for Computer Programming» («Una base axiomática para la programación computacional»), introdujo un sistema formal con un conjunto de reglas lógicas aplicadas sobre declaraciones en un lenguaje determinado para verificar la correctitud de un algoritmo (se le conoce como lógica de Hoare o lógica de Floyd-Hoare).

Básicamente es una forma de axiomatizar un algoritmo. Se le dice «Hoare Triple» a la fórmula {ϕ 1} A {ϕ 2}, donde A es un algoritmo definido en algún lenguaje formal imperativo, ϕ 1es una precondición y ϕ 2una poscondición. (En la literatura se usa la palabra «program» [que vendría siendo un programa computacional] en vez de «algoritmo», dado que se enfoca más en un conjunto de estos últimos; en nuestro caso, para simplificar esto, usaremos solamente «algoritmo».)

Por ejemplo, podemos crear la gramática de un simple lenguaje imperativo utilizando la notación EBNF (esta la veremos en detalle en el capítulo 4):

Así, esta gramática puede soportar, por ejemplo, los siguientes códigos fuente:

A continuación, veamos cuatro ejemplos —bastante triviales pero instructivos— donde podemos verificar un posible defecto en un algoritmo escrito en este lenguaje usando la lógica de Hoare: