文章基本信息

标题：Coq Support in HAHA
本地全文：下载
作者：Jacek Chrzaszcz ; Aleksy Schubert ; Jakub Zakrzewski 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：97
页码：1-26
DOI：10.4230/LIPIcs.TYPES.2016.8
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：HAHA is a tool that helps in teaching and learning Hoare logic. It is targeted at an introductory course on software verification. We present a set of new features of the HAHA verification environment that exploit Coq. These features are (1) generation of verification conditions in Coq so that they can be explored and proved interactively and (2) compilation of HAHA programs into CompCert certified compilation tool-chain. With the interactive Coq proving support we obtain an interesting functionality that makes it possible to carefully examine step-by-step verification conditions and systematically discover flaws in their formulation. As a result Coq back-end serves as a kind of specification debugger.
关键词：Hoare logic; program verification; Coq theorem prover; teaching