An Interaction Concept for Program Verification Systems with Explicit Proof Object

摘要

Deductive program verification is a difficult task: in general, user guidance is required to control the proof search and construction. Providing the right guiding information is challenging for users and usually requires several reiterations. Supporting the user in this process can considerably reduce the effort of program verification. In this paper, we present an interaction concept for deductive program verification systems that combines point-and-click interaction with the use of a proof scripting language. Our contribution is twofold: Firstly, we present a concept for a flexible and concise proof scripting language tailored to the needs of program verification. Secondly, we explore the correspondences between program debugging and proof debugging and introduce a concept for analysing failed proof attempts which leverages well-established concepts from software debugging. We illustrate our concepts on examples - including small Java programs with non-trivial specifications - using an early prototype implementation of our interaction concepts that is built on top of the program verification system KeY.