Package org.jmlspecs.jmldoc.jmldoc_142

Class Summary

JmlClassDoc
JmldocClassSubWriter
JmldocClassWriter	A derivative of a class in the javadoc doclet API, so as to be able to instantiate a MjdocClassWriter instead of a ClassWriter and a MjdocMethodSubWriter instead of a MethodSubWriter.
JmldocClassWriter.JmlMemberFilter
JmldocConstructorSubWriter	This is an extension of the doclet api in order to provide functionality for writing JML annotations.
JmldocFieldSubWriter
JmldocGUI	This class is automatically generated from JmldocGUI.gui and contains member fields corresponding to tool-specific GUI specifications.
JmldocMethodSubWriter	This is an extension of the doclet api in order to provide functionality for writing external methods.
JmldocStandard	The class with "start" method, calls individual Writers.
JmldocWrapper
JmldocWrapper.JmlCClassMap
JmldocWrapper.RefinementWrapper
JmlHTML	This class contains functions to generate html, fitting in with javadoc comments, that documents jml annotations.
JmlHTML.IntPair	This class holds a pair of integers, used here to mark the start and (one past the) end of a section of a text string.
JmlHTML.IntString	This class holds an integer and a String, corresponding to a position at which to insert text, and the text to be inserted at that position.
JmlHtmlFactory	This class is just used to create a factory instance of the JmlHTML class, from which one can call jmlize to do the actual work on a real file.
Main	This class implements the entry point of the JML compiler.
Main.JmlPrivacyChecker
SpecWriter	This class is a Visitor class that generates appropriate portions of the javadoc documentation by walking the parse tree.