Verificación de programas

Abstract

[en] Hoare’s logic is one of the main methods for verifying the partial correctness of programs. With it, it can be reasoned whether, starting from some initial conditions and assuming the execution ends, an output that meets the expected final conditions can be obtained. The main objective of this paper is to study the soundness, incompleteness and completeness in the sense of Cook of Hoare’s system. In addition, other methods related to program verification and program termination will be presented, accompanied by practical examples.

[es] La lógica de Hoare es uno de los métodos principales para la verificación de la corrección parcial de programas. Con ella se puede razonar si partiendo de unas condiciones iniciales y suponiendo que termina la ejecución, se puede obtener una salida que cumpla las condiciones finales esperadas. El objetivo principal de este trabajo es estudiar la corrección, la incompletitud y la completitud en el sentido de Cook del sistema de Hoare. Además se presentarán otros métodos relacionados con la verificación y la terminación de programas acompañados de ejemplos prácticos.