  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.
