A Teaching Tool for Mathematical Reasoning

.
One of the objectives of all undergraduate curricula in computer science and courses in discrete mathematics is to at least expose students to symbolic, mathematical reasoning. One obvious approach to motivate and teach reasoning is in the context of establishing software correctness and proving that a given implementation satisfies its specification.

A tool to teach mathematical reasoning is available at this link. The system is set up to allow creation, experimentation, and education with a variety of mathematical structures, software components, and exercises. The RESOVE verification condition generator (verifier) takes an implementation and corresponding specification(s) to form conditions which must be proved to show the correctness of the implementation. The verification generator is based on an imperative programming language RESOLVE, which has been designed for the purpose of verification. The details for the programming and specification languages can be found at www.clemson.edu/~resolve.

The Basic Idea with Examples

Given below are two example specifications of operations in the RESOLVE notation. All specifications rely on mathematical conceptualization (or modeling) of programming objects. In the first example, programming integers are mathematically conceptualized as taking values from Z. In the example specification below, parameters I and J are updated. The ensures clause of the operation states that at the end of the operation the parameter I will have the incoming value of J, denoted by #J, and J will have #I as its value. There are no preconditions for this code. In the code, “:=” is function assignment. Does the code meet the specification? Answering this question intuitively is the first reasoning exercise.

Specification:
Operation Exchange(updates I, J: Integer);
ensures I = #J and J = #I;

Code:
Procedure Exchange(updates I, J: Integer);
I := Sum(I, J);
J := Difference(I, J);
I := Difference(I, J);
End Exchange;

To check the answer to this question, verification conditions can be generated using our tool. If all the conditions can be proved, then the code would be correct. A first reasoning exercise is to attempt to prove these conditions. The conditions can be understood noting that the type Integer is a computational, and therefore, its values are constrained to be within Min_Int and Max_Int. In addition, Min_Int and Max_Int themselves are constrained to be meaningful: Min_Int <= 0 < Max_Int.

Here are the verification conditions:

((((min_in <= 0) and (0 < max_int)) and (min_int> <= 0) and
(0 < max_int)) and (((min_int <= J) and (J <= max_int)) and
((min_int <= I) and (I <= max_int))))
===========================================================>
(min_int <= (I + J)) and ((I + J) <= max_int)


((((min_int <= 0) and (0 < max_int)) and (min_int <= 0) and
(0 < max_int)) and (((min_int <= J) and (J <= max_int)) and
((min_int <= I) and (I <= max_int))))
===========================================================>
(min_int <= ((I + J) - J)) and (((I + J) - J) <= max_int)


((((min_int <= 0) and (0 < max_int)) and (min_int <= 0) and
(0 < max_int)) and (((min_int <= J) and (J <= max_int)) and
((min_int <= I) and (I <= max_int))))
===========================================================>
(min_int <= ((I + J) - ((I + J) - J))) and (((I + J) - ((I + J) - J)) <= max_int)


((((min_int <= 0) and (0 < max_int)) and (min_int <= 0) and
(0 < max_int)) and (((min_int <= J) and (J <= max_int)) and
((min_int <= I) and (I <= max_int))))
===========================================================>
((I + J) - J) = I


((((min_int <= 0) and (0 < max_int)) and (min_int <= 0) and
(0 < max_int)) and (((min_int <= J) and (J <= max_int)) and
((min_int <= I) and (I <= max_int))))
===========================================================>
((I + J) - ((I + J) - J)) = J


The next reasoning question is to see what can be done to make the code correct. This can be accomplished by tightening the specification (e.g., with a requires clause) or fixing the implementation, or using a combination.

Data Abstraction Examples

Generate verification conditions and check the correctness of the following:

Specification:
Operation Flip(updates S: Stack);
ensures S = Rev(#S);

Code:
Procedure Flip(updates S: Stack);
Var S_Reversed: Stack;
Var Next_Entry: Entry

While (Depth /= 0)
changing S, S_Reversed, Next_Entry;
maintaining #S = Reverse(S_Reversed) o S;
decreasing |S|;
do
Pop(Next_Entry, S); Push(Next_Entry, S_Reversed);
end;
S_Reversed :=: S;
End Flip;

Experimentation and Tools

A tool to teach specification understanding and reasoning exercises, along with the flexibility to add several more is available. We have used the tool in our software engineering classrooms at Clemson, but classes on data structures, algorithms, and programming with objects can use the tool as well. Please also check here for additional exercises.

We appreciate your feedback on this tool as well as suggestions for several more exercises. Please contact Heather Harton or Murali Sitaraman.

This research is funded in part by a National Science Foundation CCLI grant.

Page last updated March 11, 2010 by Chuck Cook