论文标题
高级计划的演绎验证框架
A Deductive Verification Framework For Higher Order Programs
论文作者
论文摘要
在本报告中，我们介绍了为APDC（ÁreaPráticade desenvolvimento课程）课程开发的初步工作。该项目的主要目标是在Why3工具之上开发一个框架，以验证有效的高阶程序。我们将解剖化作为从高阶OCAML实现到一阶的中间转换。我们翻译的目标是WhyMl，Why3的编程语言。我们认为，已解除化可以是对高阶程序自动验证的有趣途径，因为人们可以使用现成的自动化程序验证器来证明生成的一阶程序的正确性。该报告还旨在向读者介绍演绎计划验证的主题，以及用于证明高阶有效程序的一些工具和概念。
In this report, we present the preliminary work developed for our research project for the APDC (Área Prática de Desenvolvimento Curricular) course. The main goal of this project is to develop a framework, on top of the Why3 tool, for the verification of effectful higher-order programs. We use defunctionalization as an intermediate transformation from higher-order OCaml implementations into first order ones. The target for our translation is WhyML, the Why3's programming language. We believe defunctionalization can be an interesting route for the automated verification of higher-order programs, since one can employ off-the-shelf automated program verifiers to prove the correctness of the generated first-order program. This report also serves to introduce the reader to the subject of deductive program verification and some of the tools and concepts used to prove higher order effectful programs.
