TVT: A SOFTWARE VERIFICATION PACKAGE FOR THE INTERACTIVE LEARNING OF FORMAL PROGRAMMING TECHNIQUES - An Educational Experience

Rafael del Vado Vírseda, Fernando Pérez Morente, Eduardo Berbis González

2012

Abstract

While Computational Logic plays an important role in several areas of Computer Science (CS), most educational software developed for teaching logic is not suitable to be used directly in other portions of the CS education domain where the application of logical notions is usually required. In this paper we describe the logic teaching tool TVT based on semantic tableaux that has been developed to help the students to use logic as a formal proof technique in other advanced topics of CS, such as the verification of algorithms, the algorithmic debugging of imperative programs, the formal design of invariants, and the design and derivation of algorithms from logical specifications, which are at the basis of the formal learning of programming techniques and good development of software. We present the design, implementation, and results of the evaluation of this tool by means of several educational experiences during the academic courses 2009/2010 and 2010/2011. From the results of these experiences we conclude that the use of the TVT tool in the current CS teaching can help our students to understand more advanced CS concepts and to clarify the formal process involved in the design and analysis of correct and efficient imperative programs.

Paper Citation

in Harvard Style

del Vado Vírseda R., Pérez Morente F. and Berbis González E. (2012). TVT: A SOFTWARE VERIFICATION PACKAGE FOR THE INTERACTIVE LEARNING OF FORMAL PROGRAMMING TECHNIQUES - An Educational Experience . In Proceedings of the 4th International Conference on Computer Supported Education - Volume 2: CSEDU, ISBN 978-989-8565-07-5, pages 77-82. DOI: 10.5220/0003894400770082

in Bibtex Style

@conference{csedu12,
author={Rafael del Vado Vírseda and Fernando Pérez Morente and Eduardo Berbis González},
title={TVT: A SOFTWARE VERIFICATION PACKAGE FOR THE INTERACTIVE LEARNING OF FORMAL PROGRAMMING TECHNIQUES - An Educational Experience},
booktitle={Proceedings of the 4th International Conference on Computer Supported Education - Volume 2: CSEDU,},
year={2012},
pages={77-82},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0003894400770082},
isbn={978-989-8565-07-5},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 4th International Conference on Computer Supported Education - Volume 2: CSEDU,
TI - TVT: A SOFTWARE VERIFICATION PACKAGE FOR THE INTERACTIVE LEARNING OF FORMAL PROGRAMMING TECHNIQUES - An Educational Experience
SN - 978-989-8565-07-5
AU - del Vado Vírseda R.
AU - Pérez Morente F.
AU - Berbis González E.
PY - 2012
SP - 77
EP - 82
DO - 10.5220/0003894400770082