Incremental Proof Development in Dafny with Module-Based Induction
CoRR(2024)
摘要
Highly automated theorem provers like Dafny allow users to prove simple
properties with little effort, making it easy to quickly sketch proofs. The
drawback is that such provers leave users with little control about the proof
search, meaning that the small changes inherent to the iterative process of
writing a proof often lead to unpredictable variations in verification time,
and eventually hard-to-diagnose proof failures. This sometimes turns the boon
of high automation into a curse, as instead of breaking early and showing
unsolved goals to the user like in Coq, proofs tend to gradually become
unstable until their verification time explodes. At this point, the absence of
a proof context to investigate often leaves the user to a painful debugging
session. In this paper, we show how to use Dafny modules to encode Coq-like
induction principles to dramatically improve the stability and maintainability
of proofs about inductive data structures.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要