Studying program correctness by constructing contracts

Because the concept of program correctness is generally taught as an activity independent of the programming process, most introductory computer science (CS) students perceive it as unnecessary and even irrelevant. The concept of contracts, on the other hand, is generally taught as an integral part of the programming process. As such, most introductory CS students have little difficulty understanding the need to establish contracts via preconditions and postconditions. In order to improve teaching program correctness concepts, we implemented ProVIDE, an enhanced integrated development environment (IDE) for Java [7]. Pro VIDE supports a modified version of the "design by contract" methodology [13] that assists its student programmers in contract construction. Rather than asking for both a precondition and postcondition for each of his/her methods, ProVIDE asks the student to simply supply a postcondition. ProVIDE then helps the student construct the appropriate precondition by leading him/her through an axiomatic proof of the correctness of the method. Thus, the proof of correctness of the method is a side-effect of the student's need to construct an appropriate precondition.