The Dafny Integrated Development Environment
The Dafny Integrated Development Environment
复制标题
Dafny 集成开发环境
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Valentin Wüstholz
中科院分区：
文献类型：
--
作者：
K. Leino;Valentin Wüstholz
近年来，程序验证器和交互式定理证明器变得越来越强大，更适合于验证大型程序或证明。这表明需要改善这些工具的用户体验，以提高生产力，并使非专家更容易使用。本文提出了一种集成的开发环境Dafny的编程语言，验证器，证明助理，解决了目前最先进的验证器中存在的问题：低响应性和缺乏支持理解非明显的验证失败。本文展示了几个新的功能，移动的最先进的接近验证环境，可以提供验证反馈，用户类型，并可以提出更多的有用信息的程序或失败的验证，在需求驱动和不显眼的方式。
In recent years, program verifiers and interactive theorem provers have become more powerful and more suitable for verifying large programs or proofs. This has demonstrated the need for improving the user experience of these tools to increase productivity and to make them more accessible to non-experts. This paper presents an integrated development environment for Dafny-a programming language, verifier, and proof assistant-that addresses issues present in most state-of-the-art verifiers: low responsiveness and lack of support for understanding non-obvious verification failures. The paper demonstrates several new features that move the state-of-the-art closer towards a verification environment that can provide verification feedback as the user types and can present more helpful information about the program or failed verifications in a demand-driven and unobtrusive way.