.png){kind=icon}
返回
Gradual Verification: Assuring Software Incrementally
.png){kind=icon}
PRE
AI
DOI：10.5381/jot.2026.25.1.a1.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
当前静态验证技术对增量性的支持不佳，导致开发者难以专注于指定和验证最重要属性与组件。动态验证方法支持增量性，但无法提供静态保证。为弥合这一差距，我们提出渐进式验证，通过允许每个断言为完整、部分或省略来支持增量性，并提供从动态到静态平滑过渡的可靠验证。我将描述一个能够验证操作堆上递归、可变数据结构的程序一阶规范的系统，展示原型工具，并分享一些实证结果。我们的方法解决了若干技术挑战，例如语义上连接抽象谓词的等价递归和同构递归解释，以及支持堆所有权的渐进式验证。这项工作为未来针对实际程序的工具奠定了基础，并支持在能够进行成本效益权衡的工程流程中进行验证。
Keyword:
Gradual verification
Dynamic and static checking
Program specification
Soundness
