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) sin concurrencia 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, conocido sobre 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 se le 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 …ver más…

Cada clase de programas se define usando una semántica operacional y se propone un sistema deductivo que permite la verificación de diversas propiedades. La Lógica de Hoare ha dado origen a diversos lenguajes de especificación, entre los que destaca CSP (Communicating Secuencial Process), un lenguaje orientado a procesos que desarrolló Hoare, el cual se usa hasta el momento para la especificación de sistemas concurrentes. CSP ha servido de base para otros lenguajes de especificación formal orientados a procesos como LOTOS (un lenguaje de la ISO para especificar sistemas concurrentes). Por otro lado la Lógica de Hoare se puede utilizar para especificación y verificación de programas secuenciales, distribuidos o concurrentes. De esta forma el conocimiento de la lógica de Hoare es importante no sólo por las aplicaciones que se derivan directamente de ella, sino también para comprender y posteriormente aplicar diversos formalismos que de ella se derivan.
La lógica de Hoare es una extensión de la lógica de predicados de primer orden para razonar sobre la corrección de programas imperativos construidos sobre una signatura (S). Esta extensión se obtiene introduciendo un lenguaje de comandos con el que se construyen los programas y una relación especial para expresar el comportamiento de un programa, así como un conjunto de reglas de cálculo para la manipulación de las expresiones de comportamiento.

Basada en la idea de diagrama de flujo anotado:

S es una “frase”