Invariants file format

To generate the "exposed" classes and interfaces, it's first necessary to create an invariants.json file containing the class invariants. (In the future this part will be partially automated). This file must be placed in the same package as the classes that it refers to.

Here is an example invariants.json:

{
    "util.Collections": {
        "AbstractList<T>": {
            "abstract": true,
            "fields": [
                "int size"
            ],
            "invariants": [
                "size >= 0"
            ]
        },
        "ArrayList<T>": {
            "fields": [
                "T[] elts"
            ],
            "extends": "AbstractList<T>",
            "invariants": [
                "elts != null",
                "size == length(elts, 0)",
                "nullAfter(elts, size)"
            ],
            "helpers": [
                "private static <T> int length(T[] ls, int last) { if (last == ls.length || ls[last] == null) return last; else return length(ls, last + 1);}",
                "private static <T> boolean nullAfter(T[] ls, int end) {for (int i = end; i < ls.length; i++) {if (ls[i] != null)return false;}return true;}"
            ]
        }
    }
}

In this example, there is a package named util.Collections, which contains at least two classes, AbstractList and ArrayList. The following items can be specified:

• abstract: boolean (default is false)
• extends: one string containing a Java class name
• fields: array of string, strings are Java single variable declarations
• invariants: array of string, strings are Java expressions which evaluate to a boolean
• helpers: array of string, strings are static helper methods that the invariants might use, on one line (sorry, JSON doesn't have multi-line strings)

Notes:

• Unused items are safe to omit.
• Classes without invariants don't need to be included, but if a field is common to a base class, it's better to list it there.
• Do not include interfaces.
• The static helper methods all go into the same class, so avoid making two with the same signature.

In a nutshell, fields is used to figure out which getters to generate, extends triggers inheritance of class invariants, and the helpers are inlined into the visitor which does the checks. Some of these things could be inferred from the source code (and might be in the future) but having them here cuts down on the amount of parsing and package searching that has to be done.

Generally speaking, if the JSON file is wrong, or there are name clashes, what will happen is that the generated code won't build. If you get generated code that doesn't build, and you're certain that it's because of those two things, please help us by filing a bug report.