Verification Condition Generation and Proving

.

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.