Estoy buscando el documento original donde Hoare (o alguien más, supongo) discute la terminación (corrección total). O cualquier otro trabajo inicial sobre la terminación de la lógica "vainilla" de Hoare (supongo que con eso me refiero a un HL para un lenguaje de juguete tipo C).
He echado un vistazo a la base axiomática para programas de computadora (PDF) (que parece ser esencialmente la lógica Hoare del sabor de corrección parcial) y una nota sobre la regla for , que menciona la prueba de una regla while, pero no puede parecer para encontrar el eslabón perdido; un documento sobre la terminación / la regla while / Corrección total.