加载中…
2025-12-23
The Design of an Interactive Proof Mode for Dafny
Ştefan CiobâcăK. Rustan M. LeinoŞtefan-Alexandru MercaşRoxana-Mihaela Timon
文献摘要
We propose to extend the Dafny system with an interactive proof mode. We present a motivating example, how the IPM works, including the main design choices we make, and a prototype implementation.
讨论
0讲解博客
生成讲解博客的中文版本
AI智能校验
生成AI智能校验的中文版本