Top Qs
Línea de tiempo
Chat
Contexto
Lógica de Hoare
De Wikipedia, la enciclopedia libre
Remove ads
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.
Remove ads
Véase también
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads