This submission contains:
- a formalisation of a small While language with support for output;
- a standard total-correctness Hoare logic that has been proved sound and complete; and
- a new Hoare logic for proofs about programs that diverge: this new logic has also been proved sound and complete.
- Åman Pohjola, J., Rostedt, H., & Myreen, M. O. (2019). Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. Schloss Dagstuhl - Leibniz-Zentrum Fuer Informatik GmbH, Wadern/Saarbruecken, Germany. https://doi.org/10.4230/LIPICS.ITP.2019.32