Logica De Hoare

Lógica de Hoare
Desarrollada por C.A.R. Hoare (1969), es una lógica que permite probar la verdad o falsedad de propiedades de programas imperativos (especialmente corrección y terminación) sinconcurrencia o paralelismo. Sir Charles Antony Richard Hoare (Colombo, Sri Lanka, 11 de enero de 1934), también conocido familiarmente como Tony Hoare, es un científico Británico en computación, conocidosobre todo por la invención, en 1960 de Quicksort, que es el algoritmo de ordenamiento más ampliamente utilizado en el mundo, y probablemente el algoritmo de cualquier tipo más utilizado. También sele conoce por el desarrollo de la Lógica de Hoare, y por el lenguaje formal CSP (tercer trabajo más citado en computación de acuerdo con las estadísticas de Citeseer), utilizado para especificarinteracciones entre procesos concurrentes que sirve de base para la definición del lenguaje de programación Occam.
La lógica de Hoare es un sistema formal desarrollado por C.A.R. Hoare yposteriormente refinado por otros investigadores que proporciona a una serie de reglas de inferencia para razonar sobre la corrección de programas imperativos con el rigor de la lógica matemática.
Esta lógicafue publicada por Hoare en 1969 donde mencionó las contribuciones de Robert Floyd, que había publicado un sistema similar para los diagramas de flujo.
La principal característica de esta lógica es laterna “{Q} S {R}”, donde Q y R son predicados lógicos que deben cumplirse para que el programa S funcione. Es decir, que si el programa S comienza en un estado válido en Q, entonces el programatermina y lo hace en un estado válido para R.
Este método de pre condición(Q) post condición(R) es la base del diseño de software por contrato.
Iniciada en 1969 para programas secuenciales y extendidopor varios investigadores a programas concurrentes, es el más aceptado y el que más influencia ha tenido en la metodología de la programación. Esta técnica plantea un sistema de axiomas y reglas de...