Tutorial implementation of Hoare logic in Haskell
Programming Languages
2021-12-28 v9 Logic in Computer Science
Abstract
Using the programming language Haskell, we introduce an implementation of propositional calculus, number theory, and a simple imperative language that can evaluate arithmetic and boolean expressions. Finally, we provide an implementation of Hoare's logic which will allow us to deduce facts about programs without the need for a full evaluation.
Keywords
Cite
@article{arxiv.2101.11320,
title = {Tutorial implementation of Hoare logic in Haskell},
author = {Boro Sitnikovski},
journal= {arXiv preprint arXiv:2101.11320},
year = {2021}
}
Comments
Added sample implementation for H-Consequence, H-While, and another example; Added CoI section, tweaks to labels for 'boptimize'; Improved Hoare logic implementation by relying on actual Propositional calculus and Number theory systems, rather than toy optimization functions; improve formula printer; small tweak updates. Associated files are available at https://github.com/bor0/hoare-imp