An Innovative Teaching Tool based on Semantic Tableaux for Verification and Debugging of Imperative Programs

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 large portions of the CS education domain where the application of logical notions is usually required. In this paper we describe an innovative methodology based on a logic teaching tool on semantic tableaux that has been developed to help 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 programs, and the derivation of algorithms from logical specifications, which are foundations of good development of software. We present the results of the evaluation of this tool by means of several educational experiences during the academic year 2009/2010. From these results we conclude that the use of the tool in current CS teaching can help our students to understand more advanced CS concepts and clarify the formal process involved in the design and analysis of correct and efficient imperative programs