Estou procurando o artigo original em que Hoare (ou outra pessoa, suponho) discute a rescisão (correção total). Ou qualquer outro trabalho inicial sobre rescisão para a lógica Hoare "baunilha" (suponho que quero dizer um HL para uma linguagem de brinquedo do tipo C).
Dei uma olhada na base axiomática de programas de computador (PDF) (que parece ser essencialmente a lógica Hoare do tipo de correção parcial) e uma nota na regra for , que menciona a prova de uma regra de tempo, mas não pode parecer para encontrar o link que faltava; um artigo sobre rescisão / regra do tempo / correção total.
reference-request
lo.logic
pl.programming-languages
program-verification
program-logic
CESally
fonte
fonte