La lógica de Hoare es un sistema formal desarrollado por C.A.R. Hoare — y posteriormente 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ógica fue 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 la terna o triplete “{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 programa termina y lo hace en un estado válido para R.

Este método de precondición(Q) - postcondición(R) es la base del diseño de software por contrato.

Véase también

• Semántica de transformación de predicados
• Verificación formal.