About this paper

Appears in:
Pages: 6260-6270
Publication year: 2013
ISBN: 978-84-616-2661-8
ISSN: 2340-1079

Conference name: 7th International Technology, Education and Development Conference
Dates: 4-5 March, 2013
Location: Valencia, Spain

APPLYING PROGRAM VERIFICATION METHODS IN SOFTWARE SPECIALISTS EDUCATION

M. Todorova

St. Kl. Ohridski University of Sofia (BULGARIA)
The article presents the applying formal program verification methods during the first years of programming education, specialty Computer Science at Sofia University. What is described are the main stages of education which includes training in verification of: procedural programming (as part of the course Introduction to Programming); object-oriented programs (as part of the course Object-Oriented Programming) and abstract data types (as part of the course Data Structures and Programming). The goals, approaches used and verification tools are given for all stages of education. The results are analyzed and presented.
Education on the subject is based on axiomatic semantics and uses the techniques of design by contract, class invariant, proving theorems and consistency check. Particular attention is paid to a specially developed, for educational purposes, approach for verification of procedural and object-oriented programs, based on generalized nets (structures similar to Petri’s nets). The approach executes separated verification of the functions and procedural program which uses them. It also performs separated verification of the classes and the object-oriented program which executes their member functions. The verification of the functions and member functions of the classes is performed through formulating and proving theorems via the HOL theorem proving system. Applying the “design by contract” concept, specifications are developed to describe the relations between procedural programs functions, or between member functions of the classes of the object oriented programs, in a form of sequences of correct calls. The consistency check is done by designing and parallel executing of generalized net models of the specifications and of the programs to be verified.
@InProceedings{TODOROVA2013APP,
author = {Todorova, M.},
title = {APPLYING PROGRAM VERIFICATION METHODS IN SOFTWARE SPECIALISTS EDUCATION},
series = {7th International Technology, Education and Development Conference},
booktitle = {INTED2013 Proceedings},
isbn = {978-84-616-2661-8},
issn = {2340-1079},
publisher = {IATED},
location = {Valencia, Spain},
month = {4-5 March, 2013},
year = {2013},
pages = {6260-6270}}
TY - CONF
AU - M. Todorova
TI - APPLYING PROGRAM VERIFICATION METHODS IN SOFTWARE SPECIALISTS EDUCATION
SN - 978-84-616-2661-8/2340-1079
PY - 2013
Y1 - 4-5 March, 2013
CI - Valencia, Spain
JO - 7th International Technology, Education and Development Conference
JA - INTED2013 Proceedings
SP - 6260
EP - 6270
ER -
M. Todorova (2013) APPLYING PROGRAM VERIFICATION METHODS IN SOFTWARE SPECIALISTS EDUCATION, INTED2013 Proceedings, pp. 6260-6270.
User:
Pass: