Experiences using SPARK in an undergraduate CS course

ABSTRACT

This paper describes experiences garnered while teaching a course on high integrity software using SPARK to a mix of junior and senior level undergraduates. The paper describes the impact of pre-requisites, course layout and execution, and lessons learned by students and the instructor. The course used the SPARK toolset provide by Praxis High Integrity Systems, and the Gnat Programming System (GPS) provided by AdaCore Technologies (ACT) under the Ada Academic Initiative Program. Details about using these tools is integrated through out the paper.

REFERENCES

• 1: Computer Accreditation Commission, Criteria for Accrediting Computing Programs. ABET Inc, Baltimore MD, 2003.
• 2: Maciej Syslo , Narsingh Deo , Janusz S. Kowalik, Discrete Optimization Algorithms with Pascal Programs, Prentice Hall Professional Technical Reference, 1983
• 3: www.gnat.com/academic_overview.php
• 4: www.praxis-his.com/sparkada/universities.asp

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Control structures; Constraints

General Terms:
Algorithms, Design, Documentation, Languages, Reliability, Theory, Verification

Keywords:
SPARK, computer science curriculum, computer science education