DATA61
Chalmers University of Technology
UNSW Sydney
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 co-induction, 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.
@inproceedings{AAmanPohjola_RM_19, address = {Portland, Oregon}, author = {{\AA}man Pohjola, Johannes and Rostedt, Henrik and Myreen, Magnus}, booktitle = {Proceedings of the 10th International Conference on Interactive Theorem Proving}, date = {2019-9-5}, doi = {https://doi.org/10.4230/LIPIcs.ITP.2019.26}, isbn = {9783959771221}, keywords = {Program verification; non-termination; liveness; {Hoare} logic}, month = sep, pages = {32:1-19}, paperurl = {https://trustworthy.systems/publications/full_text/AAmanPohjola_RM_19.pdf}, publisher = {LIPIcs}, title = {Characteristic Formulae for Liveness Properties of Non-terminating {CakeML} Programs}, volume = {141}, year = {2019} }