Diogenes: finding honest Java programs (without a lamp)ΒΆ

Diogenes is a tool which supports programmers in writing honest contract-oriented Java programs. In this context, honesty means always respecting the contracts one advertises, in all possible execution contexts. Honest programs are never sanctioned by the contract-oriented infrastructure; further, compositions of honest services are deadlock-free.

The main features of Diogenes are:

  • an Eclipse plugin to write CO2 specifications of services
  • an honesty checker for CO2 specifications
  • a translator from CO2 to Java programs interacting with the contract-oriented infrastructure
  • an honesty checker for Java programs upon refinement