La historia del desarrollo de la metodología de programación.

Desde la década de 1950 hasta principios de la de 1960, Knuth llamó a los programas una obra de arte debido al enfoque artesanal de la programación.

Desde finales de los años 1960 hasta principios de los 1970 se produjo una crisis del software: por un lado, se requirieron una gran cantidad de sistemas de software, como sistemas operativos y sistemas de gestión de bases de datos, por otro lado, software; Los ciclos de desarrollo eran largos, la confiabilidad era pobre y el mantenimiento era difícil. El enfoque de la programación: espero escribir un programa con una estructura clara, fácil de leer, fácil de modificar y fácil de verificar, es decir, un programa con una buena estructura.

En 1968, la Organización del Tratado del Atlántico Norte (OTAN) celebró la primera conferencia de ingeniería de software en Alemania Occidental. En ella se analizó la situación de crisis, se estudiaron las causas fundamentales del problema y se propuso el uso de la ingeniería para la solución. Por primera vez, para resolver los problemas del desarrollo y la producción de software, esta conferencia puede considerarse como un hito importante en la historia del desarrollo de software.

En 1969, la Asociación Internacional para el Procesamiento de Información (IFIP) estableció el "Grupo de Trabajo de Metodología de Programación" para especializarse en el estudio de la metodología de programación. La programación ha pasado de un enfoque manual a un enfoque de ingeniería. 1968. Un estudio de métodos de programación estructurada. Dijkstra propuso "GOTO es dañino", con la esperanza de garantizar la corrección del funcionamiento dinámico del programa a través de una buena estructura estática del programa.

En 1969, Wirth propuso el principio de "refinamiento de arriba hacia abajo, paso a paso, divide y vencerás" para el diseño de grandes programas. La idea básica es: comenzar desde el problema original a resolver, utilizar métodos científicos abstractos, descomponerlo en una serie de pequeños problemas relativamente independientes y refinarlos uno por uno hasta que se resuelva cada pequeño problema. En 1967, Floyd propuso utilizar el "método de afirmación" para demostrar la exactitud de los programas de diagramas de bloques.

En 1969, Hoare definió un lenguaje pequeño y un sistema lógico basado en Floyd. Este sistema lógico contiene axiomas del programa y reglas de derivación, con el propósito de demostrar la corrección parcial del programa. Esta es la famosa lógica de Hoare. Su trabajo sentó las bases para el estudio de la semántica axiomática.

En 1973, Hoare y Wirth axiomatizaron la mayor parte del lenguaje PASCAL.

En 1975 apareció por primera vez un sistema de verificación automática basado en axiomas y reglas de derivación.

En 1979 apareció el lenguaje de programación Euclides definido por el pensamiento axiomático.

En 1976, Dijkstra propuso los conceptos de predicado más débil y convertidor de predicados, que se utilizan para demostrar la corrección de los programas y formalizar la derivación de programas.

En 1980, D. Gries sintetizó un sistema de demostración basado en el cálculo de predicados y lo llamó "ciencia de la programación". Por primera vez, la programación ha pasado de la experiencia y la tecnología a la ciencia.

En 1974, la gente utilizó la lógica modal para verificar la corrección de programas paralelos.

Controversia sobre la prueba de la corrección del programa:

Dudas y objeciones, razones: Primero, la prueba formal es demasiado complicada. ¿Quién puede garantizar que la prueba en sí esté libre de errores? En segundo lugar, demostrar la exactitud del programa después de escribirlo equivale a "retrospectiva", es decir, se ha cometido el error, ¿cómo se puede corregir probándolo?

Un compromiso: escribir el programa y pensar en la prueba. Es decir, el diseño del programa y la prueba de corrección se consideran simultáneamente y en paralelo. Utilizando el convertidor de predicados de Dijkstra y su conjunto de reglas de cálculo, se pueden derivar programas correctos.

Utilizar cambios de programa para construir programas correctos. Aplica una serie de reglas de transformación para proteger la corrección del programa y finalmente obtiene un programa ejecutable. La transformación de programas ha sido un aspecto importante de la investigación sobre "metodología de programación" desde la década de 1970 y es una de las formas prometedoras de automatizar el diseño de programas. La transformación recursiva del programa fue el logro más significativo de este período. Como el sistema de transformación de programas recursivo de Burstall y Darlington.

La programación lógica y la programación funcional representan una nueva dirección de investigación. Prolog es un sistema formal basado en un subconjunto de lógica de predicados (cláusulas de Hoare). El proceso de ejecución de Prolog es el proceso de ejecutar el algoritmo de digestión lógica. Los tipos de datos abstractos son un método extremadamente importante en la metodología de programación. La gente lo considera un hito importante en la historia del desarrollo de la metodología de programación.