Listado 1. Aplicación de aspectos y DbC con Ptolemy

ptolemy.java

// El evento se notifica cuando Entero cambia
void event IntEvento {
  // variables de contexto
  int x,y; 
  // Contrato translúcido. Iniciamos con precondición.
  requires x < 25 &&  y < 120 
  assumes {
    next.invoke();
    establishes next.x() == old(next.x());
  }
  ensures x < 25
  // Cerramos con postcondición.
}

public class Entero {
  Entero() {
    // Registra el evento en la lista de los objetos activos.
    register(this); 
  }
  
  public void aviso(IntEvento next) throws Throwable {
    next.invoke();
    // Refinamiento contrato translúcido
    refining establishes next.x() == old(next.x()) { 
      System.out.println("Valor x: "+ next.x() + "\nValor y:"+next.y());
    }
  }
  when IntEvento do aviso;
  
  void metodo() {	
    // activación del aspecto
    announce IntEvento(20,119) {
      System.out.println("Hola!! cumplo el contrato traslucido");
    }
    announce IntEvento(200,12) { 
      System.out.println("No cumplo el contrato translúcido");
    }
  }
  
  public static void main(String[]args) {
    new Entero().metodo();
  }

}