Premium
Integrated program verification tools in education
Author(s) -
Caso Guido,
Garbervetsky Diego,
Gorín Daniel
Publication year - 2013
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/spe.2143
Subject(s) - computer science , compiler , programming language , correctness , software engineering , field (mathematics) , eclipse , semantics (computer science) , physics , mathematics , astronomy , pure mathematics
SUMMARY Automated software verification is an active field of research, which has made enormous progress both in theoretical and practical aspects. Even if not ready for large‐scale industrial adoption, the technology behind automated program verifiers is now mature enough to gracefully handle the kind of programs that arise in introductory programming courses. This opens exciting new opportunities in teaching the basics of reasoning about program correctness to novice students. However, for these tools to be effective, command‐line‐style user‐interfaces need to be replaced. In this paper, we report on our experience using the verifying compiler for PEST in an introductory programming course as well as in a more advanced course on program analysis. PEST is an extremely basic programming language, but with expressive annotations capabilities and semantics amenable to verification. In particular, we comment on the crucial role played by the integration of this verifying compiler with the Eclipse integrated development environment. Copyright © 2012 John Wiley & Sons, Ltd.