Runtime Verification of Computer Programs and its Applicationin Programming Education

Abstract

The paper presents a technique for runtime program verification and its application in computer programming education. This approach is experimentally introduced in computer science curricula at Faculty of Mathematics and Informatics, Sofia University "St. Kliment Ohridski". Runtime verification combines formal verification methods with program execution. The proposed formal verification method is based on axiomatic semantics, enriched with techniques such as design by contract and class invariant. Specification of pre- and post- conditions, the invariants, and the loop termination functions are implemented by assertions. The presented approach is illustrated by examples for runtime verification for both traditional procedural programs, and object-oriented programs in C++ programming language.