Serializing Mathematical Formulas

This article explains how to serialize and de-serialize typed mathematical formulas, that is instances of class org.eventb.core.ast.Formula which have been type-checked.

Serialization

To serialize a typed formula, it is not sufficient to only serialize the formula. One also needs to serialize its type environment. Hopefully, this is quite easy to do. Suppose you want to save a formula as an array of strings. Here is the code to do it:

        final List<String> strings = new ArrayList<String>();

        // Serialize predicate
        assert foo.isTypeChecked();
        strings.add(foo.toStringWithTypes());

        // Serialize type environment
        for (final FreeIdentifier i : foo.getFreeIdentifiers()) {
            strings.add(i.getName());
            strings.add(i.getType().toString());
        }

De-serialization

To de-serialize a typed formula, one just performs the same steps in the reverse order. Here we assume that the formula is a predicate and has been serialized to an array of strings.

        // De-serialize type environment
        final FormulaFactory ff = FormulaFactory.getDefault();
        final ITypeEnvironment typenv = ff.makeTypeEnvironment();
        final int size = strings.size();
        for (int i = 1; i < size; i += 2) {
            final String name = strings.get(i);
            final Type type = ff.parseType(strings.get(i + 1)).getParsedType();
            typenv.addName(name, type);
        }

        // De-serialize predicate
        final Predicate bar = ff.parsePredicate(strings.get(0))
                .getParsedPredicate();
        bar.typeCheck(typenv);
        assert bar.isTypeChecked();