With the progress in deductive program verification research, new tools and techniques have become available to support design-by-contract reasoning about non-trivial programs written in widely-used programming languages. However, deductive program verification remains an activity for experts, with ample experience in programming, specification and verification. We would like to change this situation, by developing program verification techniques that are available to a larger audience. In this paper, we present how we developed prototypal program verification support for Snap!. Snap! is a visual programming language, aiming in particular at high school students. We added specification language constructs in a similar visual style, designed to make the intended semantics clear from the look and feel of the specification constructs. We provide support both for static and dynamic verification of Snap! programs. Special attention is given to the error messaging, to make this as intuitive as possible.
翻译：随着减税方案核查研究的进展,新的工具和技术已经能够用来支持以广泛使用的编程语言编写的非三边程序逐项设计推理;然而,减税方案核查仍然是专家的一项活动,在编程、规格和核查方面经验丰富。我们希望通过开发可供更多受众使用的程序核查技术来改变这种情况。在本文件中,我们介绍我们如何为Snap开发原生程序核查支持!Snap!Cap!是一种视觉编程语言,特别针对高中学生。我们添加了类似视觉风格的规格语言结构,旨在将预定的语义从规格结构的外观和感觉中弄清楚。我们既支持静态又动态地核查“吸附”方案。我们特别注意错误信息,尽可能直观地进行。
相关内容
微信扫码咨询专知VIP会员