Using SPARK for a beginner's course on reasoning about imperative programs

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. practical work.

REFERENCES

• 1: John Barnes, High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 2: Isabelle Dony , Baudouin Le Charlier, A tool for helping teach a programming method, Proceedings of the 11th annual SIGCSE conference on Innovation and technology in computer science education, June 26-28, 2006, Bologna, Italy
• 3: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 4: K.-K. Lau. A beginner's course on reasoning about imperative programs. In C. Dean and R. Boute, editors, Proceedings of Symposium on Teaching Formal Methods 2004, Lecture Notes in Computer Science 3294, pages 1--16. Springer-Verlag, 2004.

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.3 COMPUTERS AND EDUCATION
      K.3.2 Computer and Information Science Education
          Subjects: Computer science education

General Terms:
Experimentation

Keywords:
imperative programming, predicate transformer semantics