Abstract

This research focuses on the implementation of a static verification method in Snap!. Snap! is a visual programming language in which a program can be made by using blocks which will form the program. This language is mainly used by high school students. Therefore an implementation of static verification in this language will be ideal to explain and demonstrate the use of static verification to students at a younger age. In this way students can understand the use of static verification in a language more appealing to them since they already are using it. To implement this static verification, a tool called Boogie [1] will be used. Boogie is an intermediate static verification tool, made by Microsoft research. This tool is meant to be used as a foundation for other static verification tools. The Snap! code will be transformed to Boogie code, which then will be checked by the Boogie verifier. This way, the goal of being able to verify Snap! programs will be achieved.