Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs
Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2019
There are useful programs that do not terminate, and yet standard Hoare logics are not able to prove liveness properties about non-terminating programs. This paper shows how a Hoare-like programming logic framework (characteristic formulae) can be extended to enable reasoning about the I/O behaviour of programs that do not terminate. The approach is inspired by transfinite induction rather than coinduction, and does not require non-terminating loops to be productive. This work has been developed in the HOL4 theorem prover and has been integrated into the ecosystem of proof tools surrounding the CakeML programming language.