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 JUMPWriter
featureCollection
- features to writedp
- 'OutputFile' or 'DefaultValue' to specify what file to write.IllegalParametersException
java.lang.Exception