Programming by contract: static verification of object-oriented programs

ir. Jonathan Luyckx

The importance of software in our current society is well established. It is also evident that we prefer software works correctly. In the real world however, this preference is not always fulfilled. There exists a large variety of anecdotical evidence about software errors and their consequences. One example is the crash of the $165.000.000 Mars Polar Lander in 1999 during it's descent to Mars. The official reason according to the MPL Investigation Board: a programming glitch resulted in the engines being shut off at about 40 meters above the surface of Mars. This anecdotical evidence however still doesn't give us a perspective on the real scale of the problem. For that, we refer to well founded research of these matters, carried out by NIST in 2002. The main conclusion: "Software Errors Cost U.S. Economy $59.5 Billion Annualy". That's about 0.6% of the gross domestic product! They further conclude that 1/3 of this total cost could be avoided by a better methodology and test-infrastructure. That is also the perspective for this thesis: the concepts of contractual programming as the methodology, and a basis for the test-infrastructure: JProver.

Contractual programming is a methodolgy originally introduced by Betrand Meyer. The basic principle is to not only write informal comments when programming, but also to supply each piece of code with a rigourously defined specification. One speaks of pre- and postconditions that respectively identify the constraints that must be met before and after executing a certain piece of code. By relying on the operations within that piece of code, and the contracts of other parts of the program used in that piece, one can formally prove the correctnes of a certain piece of software. This proof however is tedious and it is not practical for a programmer to produce this proof during development. In this thesis, a tool is developed that makes it possible to provide such a proof automatically.

More specifically, this thesis builds upon an earlier effort on static verification: JProver. This tool has been thoroughly extended, to support the semantics of object-oriented programming. Furthermore, JProver has been made completely language independent by basing it on a generic metamodel of object-oriented programs, chameleon. The largest contribution however has been the development of a complete new theorem prover, a system that can automatically produce a proof of a mathematical proposition. A theorem prover is required to conduct static verification, and directly affects the capabilities of such a verification system. The original version of JProver was in this regard limited by it's use of an existing theorem prover. The new prover is based on term rewriting, resolution and ordered paramodulation. These concepts have been combined with a new method of integrating heuristic knowledge of the programming code in the resolution process. That results in a better time-! complexity for these proofs, and essentially means the ability to prove the correctness of more complex programs.