Serializing Mathematical Formulas - Revision history

imported>Mathieu at 11:02, 10 November 2008

2008-11-10T11:02:07Z

← Older revision		Revision as of 11:02, 10 November 2008
Line 1:		Line 1:
	This article explains how to serialize and de-serialize typed mathematical formulas,		This article explains how to serialize and de-serialize typed mathematical formulas, that is instances of class {{class\|org.eventb.core.ast.Formula}} which have been type-checked.
	that is instances of class {{class\|org.eventb.core.ast.Formula}} which have been type-checked.

	==Serialization==		==Serialization==

imported>Mathieu at 11:01, 10 November 2008

2008-11-10T11:01:53Z

← Older revision		Revision as of 11:01, 10 November 2008
Line 1:		Line 1:
	This article explains how to serialize and de-serialize typed 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.		that is instances of class {{class\|org.eventb.core.ast.Formula}} which have been type-checked.

	==Serialization==		==Serialization==

imported>Mathieu: From http://rodin-b-sharp.wiki.sourceforge.net/Serializing+Mathematical+Formulas

2008-11-10T11:01:29Z

From http://rodin-b-sharp.wiki.sourceforge.net/Serializing+Mathematical+Formulas

New page

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:
<pre>
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());
}
</pre>

==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.
<pre>
// 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();
</pre>

[[Category:Developer documentation]]