Teaching and Assessment of Logical Reasoning Skills
Ubiquity of computing makes the need for software that functions correctly apparent. Skills for analytical reasoning of software correctness are central for the next generation of students. This project has taken an important step in engaging students in reasoning and in assessing that reasoning skills are successfully learnt.
The overall goal of the project is to teach mathematical reasoning principles across the curriculum, assess the effectiveness of student learning, institutionalize the principles at Clemson, and disseminate the results for use by other institutions. The project goals also include design, development, and use of a web-integrated reasoning environment for education.
At Clemson, reasoning concepts have been included in the syllabi of two required courses for CS majors. A full-fledged web-integrated environment for reasoning has been developed and used at Clemson and other institutions. To facilitate systematic assessment, an Inventory of Reasoning about Correctness Principles has been developed and employed. Using the inventory, specific learning outcomes and assessment questions have been developed.
Establishment of the idea that anayltical reasoning principles can be taught effectively and in an engaging manner through multi-year assessment is the most significant outcome. Development of features within the web IDE to support the reasoning process and development of RCI tests for continuous assessment and improvement are other important outcomes.
The ideas have been institutionalized at Clemson. The results have been disseminated to over 100 professors through a dozen workshops; several professors have adapted the principles for use at their institutions.
Only selected publications from 2014 and 2015 are listed.
Svetlana V. Drachova, Joseph E. Hollingsworth, Joan Krone, Jason O. Hallstrom, Rich Pak, and Murali Sitaraman (2015). Teaching Mathematical Reasoning Principles of Software Correctness and Its Assessment. ACM Transactions on Computing Education.
Joseph Hollingsworth and Murali Sitaraman (2015). Evaluation of Formal Reasoning Abilities Using a Concept Inventory. 1st Formal Methods in SW Engineering Education and Training Workshop, Co-located with FM 2015. Oslo, Norway.
Nabil M. Kabbani, Daniel Welch, Caleb Priester, Stephen Schaub, Blair Durkee, Yu-Shan Sun, and Murali Sitaraman (2015). Formal Reasoning Using an Iterative Approach with an Integrated Web IDE. 2nd Workshop on Formal-IDE: A satellite workshop of FM 2015. Oslo, Norway.
Charles T. Cook, Yu-Shan Sun, and Murali Sitaraman (2014). Experience Report: Evolution of a Web-Integrated Software Development and Verification Environment. Wiley Software: Practice and Experience.
Jason O. Hallstrom, Cathy Hochrine, Jacob Sorber, Murali Sitaraman (2014). An ACM 2013 exemplar course integrating fundamentals, languages, and software engineering. ACM SIGCSE. Atlanta, GA.
Murali Sitaraman and Bruce W. Weide (2014). Special session: 'Hands-on' tutorial: Teaching software correctness with RESOLVE. ACM SIGCSE. Atlanta, GA.
Joseph E. Hollingsworth and Murali Sitaraman (2014). Special session: Engaging mathematical reasoning exercises. ACM SIGCSE. Atlanta, GA.
Actively Learning Logical Reasoning about Code
Students typically learn to reason about code by writing code, running it on example test inputs, and understanding whether the outputs produced by the programs match their expectations. This understanding is limited to the examples used an may not lead to an overall logical understanding of the code. The logical reasoning tool presented benefits beginning programmers as well as software engineering students.
This paper will discuss an integrated development environment (IDE) for logical reasoning about code correctness. The IDE allows students to be actively engaged in learning. A version of the IDE has been integrated with the web to facilitate online learning and has been used in classrooms for nearly 5 years.
The IDE is supported by a logical verification engine that has funded by an NSF CCF grant. Students have used the IDE for classroom logical reasoning and for software engineering projects. Benefits have been assessed through surveys.
The web IDE allows students to explore and ask 'what if' questions, and learn logical reasoning about code correctness at a foundational level. It enhances student engagement through active learning.
The web IDE has been used for multiple years in a required software engineering course at Clemson, and at related courses in a few other institutions. The online presence makes it possible to reach a diverse audience and achieve a broader impact.