Incremental Certified Programming

Tomás Díaz

doi:10.1145/3763068

2025-10-01

PRE

DOI：10.1145/3763068

原文求助

摘要

En 中文

认证编程，如在证明助手和依赖类型编程语言中实施的那样，通过支持规范和证明的定义，确保软件满足其需求。然而，由于规范并未设计为考虑程序的不完整中间状态，证明在部分定义和增量更改下容易失效。我们通过分析其目标和固有挑战，倡导对增量认证编程提供适当支持，并提出一个正式框架，以原则性方式实现增量认证编程。关键思想是定义适当的完备性精化和完备性概念以捕捉增量性，并系统地生成在开发各阶段均有效的规范，同时保留原始陈述的意图。我们在Rocq证明器中提供了一个名为IncRease的原型实现，该实现利用类型类进行自动化和可扩展性，且独立于任何用于处理不完备性的特定机制。我们通过一个逐步增加的简单类型lambda演算教科书形式化以及CompCert项目中现有死代码消除优化传递的更复杂增量认证编程案例研究来说明其用法。我们证明该方法与QuickChick提供的随机属性基础测试兼容。最后，我们研究如何结合增量认证编程与演绎综合，使用Fiat库的新型增量友好适配。这项工作为系统化支持增量认证编程提供了理论基础和实践基础，突出了未来发展的挑战和前景。

Keyword:

incremental programming

program verification

theorem proving