Slide 11.5: Proofs of program correctness

Slide 11.4: While-statements
Slide 11.6: Example I of program correctness
Home

Proofs of Program Correctness

A “correct” program is one that does exactly what its designers and users intend it to do—no more and no less.

“Testing can show the presence of errors, but not their absence.” E. W. Dijkstra

Modern software systems have millions of lines of code, representing thousands of semantic states and state transitions. This innate complexity requires that designers use robust tools for assuring that the system behaves properly in each of its states. Practical proofs of program correctness are evolved as follows:

Software modeling languages had been developed as separate tools, and were not fully integrated with popular compilers and languages used by real-world programmers. Instead, these languages, like the Universal Modeling Language (UML), provide a graphical tool that includes an Object Constraint Language (OCL) for modeling properties of objects and their interrelationships in a software design.

With the emergence of Eiffel, ESC/Java, Spark/Ada, JML, and the notion of design by contract, this situation is changing rapidly. These new developments provide programmers with access to rigorous tools and verification techniques that are fully integrated with the runtime system itself. ESC/JAVA is a code-level language for annotating and statically checking a program for a wide variety of common errors.

The Java Modeling Language (JML) provides code level extensions to the Java language so that programs can include such formal specifications and their enforcement at run time.

The theory of axiomatic semantics was developed as a tool for proving the correctness of programs and program fragments, and this continues to be its major application.