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.

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:

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:

#### 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.

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.

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

Code:
**Procedure** Exchange(**updates** I, J: Integer);
**End** Exchange;

I := Sum(I, J);

J := Difference(I, J);

I := Difference(I, J);

J := Difference(I, J);

I := Difference(I, J);

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.

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

Code:
**Procedure** Flip(**updates** S: Stack);
**End** Flip;

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**
**end**;

S_Reversed :=: S;

Var Next_Entry: Entry

Pop(Next_Entry, S);
Push(Next_Entry, S_Reversed);

S_Reversed :=: S;

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