RESOLVE Demos

Engaging in Logical Code Reasoning with an Activity-Based Online Tool

Jason O. Hallstrom (Florida Atlantic University )
Joseph E. Hollingsworth (Rose-Hulman)
Megan Fowler, Eileen Kraemer and Murali Sitaraman (Clemson University)

Overview of the demo

Suitable for high school and introductory college CS courses to software engineering courses.

Typical code reasoning involves running code on specific input values and studying outputs. However, this provides limited understanding of the overall space of behaviors of the code. So, how do we learn to reason about code on all inputs? This presentation provides an overview of what you will find in the videos below.

Motivation

In this video, Jason Hallstrom provides the motivation for engaging in logical code reasoning with an activity-based online tool:
https://www.youtube.com/watch?v=ehlgP4hD_Ek&feature=youtu.be

What is symbolic reasoning?

Here, Megan Fowler provides describes what we mean by symbolic reasoning and introduces the "Begin to Reason" tool.

Video: Symbolic Reasoning

Tool: Begin to Reason

Reasoning activities

Here, Murali Sitaraman presents:

• Introductory Activities
• Advanced Activities: Loop Invariants
• Advanced Activities: Design by Contract

You can follow along in the RESOLVE Web IDE. To find it, either search in a web browser for "Clemson RESOLVE" to find the tools, or go directly to: /

---