public class JMLWriter extends java.lang.Object implements JUMPWriter
JUMPWriter specialized to write JML.
This is a simple class that passes the work off to the GMLWriter class that
knows how to auto-generate a JML compatible GMLOutputTemplate.
DataProperties for the JMLWriter write(DataProperties) interface:
| Parameter | Meaning |
|---|---|
| OutputFile or DefaultValue | File name for the output JML file |
| Constructor and Description |
|---|
JMLWriter()
Creates new JMLWriter
|
| Modifier and Type | Method and Description |
|---|---|
void |
write(FeatureCollection featureCollection,
DriverProperties dp)
Writes the feature collection to the specified file in JML format.
|
public void write(FeatureCollection featureCollection, DriverProperties dp) throws IllegalParametersException, java.lang.Exception
write in interface JUMPWriterfeatureCollection - features to writedp - 'OutputFile' or 'DefaultValue' to specify what file to write.IllegalParametersExceptionjava.lang.Exception