Welcome to XJML project

EDarío

XJML 1.0 is a platform for Verification and Validation of Java classes. Nowadays XJML 1.0 can reads one Java class and its contract (written in XML) and then executes the next verification techniques:

  1. Runtime Assertion Checking (RAC). Using JML4c and JML4rt tools.
  2. Extended Static Checking (ESC). Using ESC/Java2.
  3. Full Static Program Verification (FSPV). Using the Why platform (tested with Why 2.30 and Why3 0.71)

XJML 1.0 uses the same modules that JML4 for RAC and ESC, but for the FSPV uses the Why platform and its related provers.


Master thesis

We provide two ways to access the Master's Thesis which explains the XJML's conception. The thesis called "Verification and validation external modular of Object Oriented Systems using Design By Contract" can be found in:

  1. PDF file
  2. HTML format

How XJML 1.0 works?

Coming soon we will add the User's Manual translated to english; Right now, we have its version in spanish. This Manual will evolve, so, we present the important changes in each version (descending sort).

User's Manual 0.2 for XJML 1.0
  • All the observations from the first version were attended, and the Manual was re-structured.

  • The User's Manual for XJML 1.0 now has five Chapters.

  • The Chapters I and II still the same ones that in the previous version, that is to say: the first Chapter presents one Java class example to verify and validate with XJML 1.0; the second Chapter describes a generic environment in which XJML 1.0 can use it.

  • The Chapter III presents the contract's structure in XJML 1.0 and the description of each tag contained in the XML contract for XJML 1.0.

  • The fifth Chapter contains license information, the distribution format, and where and how get XJML 1.0. And finally, describes how uses XJML 1.0 through the Eclipse IDE.

  • The last Chapter (Chapter V) presents the contract to verify and validate the Java class AccountBank. This java class is the example case. Also contains the AccountBank and the linking class.

User's Manual 0.1 for XJML 1.0
  • Esta primera versión está compuesta por tres Capítulos.

  • El primer Capítulo presenta un ejemplo de una clase para verificar y validar con XJML 1.0.

  • El segundo Capítulo describe un entorno genérico bajo el cual XJML 1.0 puede utilizarse. En este Capítulo aún falta asignar el nombre a la clase que enlaza el contrato y la clase a verificar.

  • El tercer y último Capítulo presenta los archivos requeridos para ejecutar XJML 1.0. Aún falta:

    1) Agregar una descripción más completa de las tres técnicas de verificación que soporta XJML 1.0
    2) Presentar la clase de ejemplo para verificar y validar usando XJML 1.0
    3) Presentar la clase que enlaza el contrato y la clase a verificar
    4) Agregar las referencias correspondientes

Information about the User's Manual 0.3 for XJML 1.0

In the next update of the manual, we will do the next tasks:

1) Una nueva página de presentación, incluyendo el nuevo icono para XJML y re-acomodando los nombres de los autores, algo más atractivo.
2) Capturas de pantalla donde se muestren los resultados de la V&V de la clase CuentaBancaria usando XJML 1.0 y cada una de las técnicas de verificación soportadas.