Programación Correcta

Programación Correcta
Información sobre la plantilla
Programacion1.jpg
Concepto:Forma correcta de programar en cualquier lenguaje.

Programación Correcta. Lo correcto en programación ha ido migrando a convertirse sólo en control de calidad. Debe ser porque la programación es mucho más compleja debido al surgimiento de paradigmas que puedan lidiar con problemas más complejos. Pero también podría ser porque hemos ido siendo más diletantes cada vez descartando lo que consideramos «incómodo» en los proyectos de Ingeniería de Software.

Lógica de hoare

La lógica de Floyd-Hoare es un sistema formal publicado en 1969 por el científico británico Hoare en el artículo Una base axiomática para la programación de computadoras El propósito del sistema es proveer un conjunto de reglas lógicas para razonar sobre lo correcto de los programas de computación con el rigor de la lógica matemática. Hoare reconoce trabajos anteriores de Robert Floyd para diagramas de flujo. Estos trabajos son métodos que establecen que de todos los posibles modelos funcionales que son soluciones a un problema determinado, uno es el más correcto, el canónico. La lógica de Hoare tiene axiomas y reglas de inferencia para todas las construcciones de un lenguaje de programación imperativo.

Teoría de pruebas

Estas teorías estaban basadas en la Teoría de Pruebas, que es una rama de la lógica matemática que establece que las pruebas son objetos matemáticos formales. William Alvin Howard estableció una correspondencia entre la lógica de la intuición y el cálculo lambda. Es decir, entre programas de computadoras y la lógica de pruebas. El cálculo lambda fue desarrollado por Haskell Curry y es un modelo análogo a la Máquina de Turing.

Dijkstra

En 1968 publica un el artículo «Un caso en contra de la instrucción GOTO» que sirvió de base al paradigma de la Programación Estructurada.  Este artículo fue publicado en la revista Communications of the ACM con el título Go To Statement Considered Harmful (La instrucción GOTO considerada dañina) porque el editor Niklaus Wirth lo cambió. Wirth es el autor del lenguaje Pascal (entre algunos otros) y lo diseñó porque los que existían no le servían para cómo él quería enseñar la programación. Philippe Kahn fue su alumno. En 1975 Dijkstra extiende la lógica de Hoare con un método para definir la semántica de un lenguaje de programación imperativa asignando a cada comando en el lenguaje un transformador de predicado correspondiente. A diferencia de muchos otros formalismos semánticos, éste no fue diseñado como una investigación de los fundamentos de la computación. Más bien, tiene el propósito de proveer a los programadores de una metodología para desarrollar sus programas como correctos por construcción en un «estilo calculacional». Desde los 70s, el mayor interés de Dijkstra se centró en la Verficación Formal .La opinión en aquel momento era que primero se debía escribir un programa y entonces proveer una prueba matemática de verificación de cuan correcto era. Sus primeras teorías apuntaban a especificar matemáticamente lo que se suponía que el programa debía hacer e ir aplicando transformaciones matemáticas a esta especificación hasta que se conviertiera en un programa que pudiera ser ejecutado. El programa resultante es entonces conocido como «correcto por construcción». La mayoría de los trabajos posteriores de Dijkstra se preocupan por modernizar este argumento matemático. En una entrevista en el 2001, establece el deseo por la .elegancia., por lo cual el enfoque correcto sería procesar mentalmente ideas en vez de intentar .manufacturar. los programas hasta que estuvieran completos. Es de notar que esta evolución de Dijkstra tiende a poner por encima la Teoría del Conocimiento de las matemáticas formales. Aunque hay que aclarar que toda la lógica formal es una aplicación de las matemáticas a la primera.

Teoría del conocimiento

Se pueden encontrar referencias de cómo la Teoría del Conocimiento se aplica a la Programación. Por ejemplo, se presenta a Concept Programming como un paradigma aparte que se basa en cómo se traducen los conceptos que que viven en la cabeza de los programadores a representaciones del espacio de código. En mi opinión, la programación correcta siempre es así.

Fuentes