自动验证高阶命令式程序的分阶段规范
摘要：高阶函数和命令式引用是许多主流语言支持的语言特性。它们的结合使得能够将代码块的引用与其环境中捕获的状态一起封装起来。高阶命令式程序具有表达性和实用性，但由于使用尚未实例化的函数参数，特别是当它们的调用可能改变由其参数捕获或可从其参数访问的内存时，会使形式化规范和推理变得复杂。 现有的用于验证高阶命令式行为的最新工作有两个限制：在没有自动化实现的情况下实现强大的理论结果，或者在强大的假设的帮助下实现自动化（例如Rust的专用类型系统）。为了在没有上述限制的情况下为命令式语言提供自动化验证解决方案，我们引入了高阶分阶段分离逻辑（HSSL），它是适用于具有类似ML的局部引用的按值调用高阶函数的Hoare逻辑的扩展。 在本文中，我们设计了一种新颖的分阶段规范逻辑，证明了其正确性，为核心类似OCaml的语言开发了一种新的自动化高阶验证器Heifer，报告了实验结果，并展示了各种调查其能力的案例研究。
作者：Darius Foo, Yahui Song, Wei-Ngan Chin
论文ID：2308.00988
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-03