Educational framework for verification of object-oriented programs
Magdalina Todorova, Kamen D. Kanev · 2012
This article presents an educational framework, designed to support knowledge acquisition and skills development pertinent to program validation and in particular to formal methods for verification of object-oriented programs. The framework is intended to span from undergraduate classes, for junior and sophomore students, up to advanced classes, for graduate students. It supports distinct levels of access targeting: i) beginner, ii) intermediate, and iii) advanced users. Background knowledge and preliminarily acquired skills, associated with each access level, are well defined and reflected into the interaction interface that the framework presents to the user. For completeness, a reference description of the formal program verification method employed in the framework is included in the text, along with the underlying mathematical means supporting the method.