Email Gateway (Jan 22 2023 at 23:34): Email Gateway (Jan 22 2023 at 23:34):From: Gerwin Klein <kleing@unsw.edu.au>
A Hoare Logic for Diverging Programs
by Johannes Åman Pohjola, Magnus O. Myreen, Miki Tanaka
This submission contains:
(1) a formalisation of a small While language with support for output;
(2) a standard total-correctness Hoare logic that has been proved sound and complete; and
(3) a new Hoare logic for proofs about programs that diverge: this new logic has also been proved sound and complete.
[https://www.isa-afp.org/entries/HoareForDivergence.html]
Enjoy!
Gerwin
Last updated: Apr 24 2024 at 08:20 UTC