Enforcing Secure Object Initialization in Java's web page

Formalization in Coq

The annotation Java package

Our on-line object initialization type checker

How to use it:

How to annotate your classes

There are several kinds of annotations.


import rawtypes.*;
import java.io.*;

class Sample{
    @Init Object f;               // default annotation

    @Pre(@Raw)                    // default annotation
    @Post(@Raw(Sample.class))     // default annotation
    Sample(@Init Object param){   // default annotation
    @Pre(@Raw(Object.class)) // non-default: we call the init method on objects
                             // partially initialized
    @Post(@Raw(Sample.class)) // non-default: the object is more initialized at
                              // the end of the method
    private void init(@Init Object param){ //default annotation
        this.f = param;
        ChangeType.SetInit(); //we declare the object as initialized

    @Pre(@Raw(Sample.class)) // non-default: we allow the method to be called on
                             // partially initialized objects, as long as this.f
                             // has been initialized
    public @Init Object getF(){ // default-annotation
        return this.f;

    public void setF(Object f){ // no annotation, setF can only be called on
                                // fully initialized objects
        this.f = f;

class Sample2 extends Sample{
        super(new Object());
        Object o = this.getF(); // allowed
        this.setF(o); // fails: the current object has not finished its
                      // construction
    void m(){
        this.setF(new Object()); // allowed: the current object has finished its
                                 // construction as it is a precondition of m
                                 // (default annotation)