jSicko

Overview

jSicko is a Java SImple Contract checKer. It works as a Java compiler plugin that processes some simple annotations representing contracts and produces runtime checks. jSicko started as one of my slack projects, in collaboration with Prof. Carlo A. Furia and it was used for many years in the context of the Software Design & Modeling course↗.

One of the peculiarities of jSicko is that contract clauses are expressed in valid Java with some conventions, and not with a specific DSL (like in the case of JML). Here’s a simple example.

Simple Example

Imagine you want to write a simple contract for a square root function. What you first have to do is define two helper methods that represent the conditions themselves. These are specification clause methods, so we use a different naming condition than usual Java methods.

1
public abstract class Math implements Contract {
2

3
    // ...
4

5
    @Pure
6
    private static boolean non_negative_arg(double arg) {
7
        return arg >= 0;
8
    }
9

10
    @Pure
11
    private static boolean approximate_returns(double returns, double arg) {
12
        return java.lang.Math.abs((returns * returns) - arg) < 0.001;
13
    }
14

15
}

Then, in the sqrt method, you can simply bind the first spec clause method (non_negative_arg) as the precondition of sqrt, and approximate_returns as its postconditon as follows:

1
    @Requires("non_negative_arg")
2
    @Ensures("approximate_returns")
3
    public static double sqrt(double arg) {
4
        return java.lang.Math.sqrt(arg);
5
    }

How does the binding to parameters happen? In general, the binding is by name. However, if you call a parameter returns, that gets bound to the return value of the method.

Even if you do not have to care about it, jSicko rewrites the method as follows:

1
  public static double sqrt(double arg) {
2
      if (!non_negative_arg(arg)) {
3
          throw new PreconditionViolation("Precondition non_negative_arg violated on method sqrt");
4
      }
5
      // some more instrumentation ...
6
      double $returns = 0;
7
      try {
8
          return $returns = java.lang.Math.sqrt(arg);
9
      } finally {
10
          if (!approximate_returns($returns, arg)) {
11
              throw new PostconditionViolation("Postcondition approximate_returns violated on method sqrt");
12
          }
13
          // some more instrumentation ...
14
      }
15
  }

Essentially, jSicko checks first the preconditions, then boxes the body of the method into a try/finally block, storing the return value into a synthetic $returns variable.