Using SPARK for a Beginner's Course on Reasoning about Imperative Programs

Kung-Kiu Lau
School of Computer Science, The University of Manchester
Oxford Road, Manchester M13 9PL, United Kingdom
{kung-kiu@cs.man.ac.uk}

Abstract:

Teaching beginners predicate transformer semantics for imperative
languages is not a trivial task. For Computer Science majors, the
teaching of the theoretical material must be supported by suitable 
practical course work. For this, we need a  suitable language with 
appropriate tool support. In this paper, we describe our experience 
of using SPARK and its tools for this purpose. Our experience has 
been a very positive one.