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