Extrait du course extended static checking for Java

1. INTRODUCTION
Static checking (ESC): “static” because the checking is per-formed without running the program, and “extended” be-cause ESC catches more errors than are caught by conventional static checkers such as type checkers. ESC uses an automatic theorem-prover to reason about the semantics of programs, which allows ESC to give static warnings about many errors that are caught at runtime by modern program-ming languages (null dereferences, array bounds errors, type cast errors, etc.). It also warns about synchronization er-rors in concurrent programs (race conditions, deadlocks).Finally, ESC allows the programmer to record design de-cisions in an annotation language, and issues warnings if the program violates these design decisions. Our first ex-tended static checker, ESC/Modula-3, has been described elsewhere [8]. This paper provides an overview of our sec-ond checker, ESC/Java. It is not our goal in this paper to give a complete description of ESC/Java, but rather to give an overview that includes citations to more complete descriptions of particular aspects of the checker.
Static checking can improve software productivity because the cost of correcting an error is reduced if it is detected early.
2. AN EXAMPLE OF USING ESC/JAVA
Perhaps the simplest way to impart a feeling for what it’s like to use ESC/Java is to present an example in some detail.
Figure 2 shows a small skeleton of a class of integer bags (aka multisets). The class provides only two operations: a bag may be constructed from an array of integers, and the smallest element of a bag may be extracted.
To invoke our checker, the user invokes it just as she would the Java compiler, but with “escjava”replacingthename of the compiler on the command line: escjava Bag.java.
In response, over about the next ten seconds on a 200 MHz
Pentium Pro PC, ESC/Java produces 5 warnings:
Bag.java:6: Warning: Possible null dereference (Null) size = input.length;
^
Bag.java:15: Warning: Possible null dereference (Null)
if (elements[i] < min) {
^
Bag.java:15: Warning: Array index possibly too large (…
if (elements[i] < min) {
^
Bag.java:21: Warning: Possible null dereference (Null)
elements[minIndex] = elements[size];
^
Bag.java:21: Warning: Possible negative array index (…
elements[minIndex] = elements[size];
^
The first of the warnings is a complaint that theBag constructor may dereference null (if it is called with a null argument). There are two reasonable responses to this: ei-ther bulletproof the constructor so it can be called with null (producing an empty bag), or forbid calling the constructor with null. For this example, we assume the user chooses the second response. Traditionally, this would involve adding an English comment “This constructor may not be called with null” and hoping that programmers writing code that uses Bagobey this requirement.
3. ARCHITECTURE
ESC/Java is the second extended static checker developed at the Systems Research Center. Its architecture is similar to that of the earlier checker [8], which targeted the Modula-3 language. Like that of traditional compilers, ESC/Java’s ar-chitecture is best thought of as a pipeline of data processing stages (see Figure 3). We describe each stage in turn.
Front End.ESC/Java’s front end acts similarly to that of a normal (Java) compiler, but parses and type checks  ESC/Java annotations as well as Java source code.

……..

Si le lien ne fonctionne pas correctement, veuillez nous contacter (mentionner le lien dans votre message)
Course extended static checking for Java (503 KO) (Cours PDF)