Class JMLWriter

java.lang.Object

com.vividsolutions.jump.io.GMLWriter

com.vividsolutions.jump.io.JMLWriter

All Implemented Interfaces:

JUMPWriter, TaskMonitorSupport

public class JMLWriter
extends GMLWriter

JMLWriter is a 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 Summary

Constructors

Constructor	Description
JMLWriter()

Method Summary

Methods inherited from class GMLWriter

format, getTaskMonitor, setTaskMonitor, toString, write, write

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

JMLWriter

public JMLWriter()