Improving reusability of software is one of the main goals of object
oriented programming. One way to reach this goal is to design very general
classes that can be instantiated in multiple ways to easily obtain concrete
components of real applications. However, another desirable quality of
software is correctness. Thus, design methods to build generic classes
should be complemented by proof techniques to support the correctness of
the methods.
  In these lectures, we demonstrate on some typical examples that
specification and verification techniques used for classical programming
can be extended to cope with generic classes and their instantiations. The
approach is not entirely formal since it is intended to be used in practice
for the construction of high quality software.
  We use the programming language Java to illustrate the approach on a
concrete basis.
  In the last part of the lectures, we investigate the use of static
analyses based on abstract interpretation to support the verification and
the optimization of Java programs built according to the generic approach.

The lectures are divided into four parts as follows :

1) Overview of inheritance and polymorphism in Java.
2) Design and instantiation of generic classes in Java.
3) Specification and verification of generic and instantiated classes in Java.
4) Automatic verification and optimization of instantiated Java classes,
based on abstract interpretation.